Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpl13 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl13 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp13 1093 | . 2 | |
2 | 1 | adantr 481 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 386 df-3an 1039 |
This theorem is referenced by: pythagtriplem4 15524 mply1topmatcl 20610 brbtwn2 25785 ax5seg 25818 br8 31646 nolt02o 31845 btwndiff 32134 ifscgr 32151 seglecgr12im 32217 atlatle 34607 cvlcvr1 34626 atbtwn 34732 3dimlem3 34747 3dimlem3OLDN 34748 4atlem3 34882 4atlem11 34895 4atlem12 34898 2lplnj 34906 paddasslem4 35109 paddasslem10 35115 pmodlem1 35132 llnexchb2lem 35154 pclfinclN 35236 arglem1N 35477 cdlemd4 35488 cdlemd 35494 cdleme16 35572 cdleme20 35612 cdleme21k 35626 cdleme22cN 35630 cdleme27N 35657 cdleme28c 35660 cdleme29ex 35662 cdleme32fva 35725 cdleme40n 35756 cdlemg15a 35943 cdlemg15 35944 cdlemg16ALTN 35946 cdlemg16z 35947 cdlemg20 35973 cdlemg22 35975 cdlemg29 35993 cdlemg38 36003 cdlemk56 36259 dihord2pre 36514 uzwo4 39221 fourierdlem77 40400 |
Copyright terms: Public domain | W3C validator |