Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpl21 | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simpl21 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp21 1094 | . 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: brbtwn2 25785 ax5seglem3a 25810 ax5seg 25818 axpasch 25821 axeuclid 25843 br8d 29422 br8 31646 nosupbnd2lem1 31861 cgrextend 32115 segconeq 32117 trisegint 32135 ifscgr 32151 cgrsub 32152 cgrxfr 32162 lineext 32183 seglecgr12im 32217 segletr 32221 lineunray 32254 lineelsb2 32255 cvrcmp 34570 cvlatexch3 34625 cvlsupr2 34630 atexchcvrN 34726 3dim1 34753 3dim2 34754 ps-1 34763 ps-2 34764 3atlem3 34771 3atlem5 34773 lplnnle2at 34827 lplnllnneN 34842 2llnjaN 34852 4atlem3 34882 4atlem10b 34891 4atlem12 34898 2llnma3r 35074 paddasslem4 35109 paddasslem7 35112 paddasslem8 35113 paddasslem12 35117 paddasslem13 35118 pmodlem1 35132 pmodlem2 35133 llnexchb2lem 35154 4atex2 35363 ltrnatlw 35470 trlval4 35475 arglem1N 35477 cdlemd4 35488 cdlemd5 35489 cdleme0moN 35512 cdleme16 35572 cdleme20 35612 cdleme21j 35624 cdleme21k 35626 cdleme27N 35657 cdleme28c 35660 cdleme43fsv1snlem 35708 cdleme38n 35752 cdleme40n 35756 cdleme41snaw 35764 cdlemg6c 35908 cdlemg8c 35917 cdlemg8 35919 cdlemg12e 35935 cdlemg16 35945 cdlemg16ALTN 35946 cdlemg16z 35947 cdlemg16zz 35948 cdlemg18a 35966 cdlemg20 35973 cdlemg22 35975 cdlemg37 35977 cdlemg27b 35984 cdlemg31d 35988 cdlemg33 35999 cdlemg38 36003 cdlemg44b 36020 cdlemk38 36203 cdlemk35s-id 36226 cdlemk39s-id 36228 cdlemk55 36249 cdlemk35u 36252 cdlemk55u 36254 cdleml3N 36266 cdlemn11pre 36499 |
Copyright terms: Public domain | W3C validator |