![]() |
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 1063 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantr 472 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 190 df-an 378 df-3an 1009 |
This theorem is referenced by: brbtwn2 25014 ax5seglem3a 25039 ax5seg 25047 axpasch 25050 axeuclid 25072 br8d 28294 br8 30467 cgrextend 30846 segconeq 30848 trisegint 30866 ifscgr 30882 cgrsub 30883 cgrxfr 30893 lineext 30914 seglecgr12im 30948 segletr 30952 lineunray 30985 lineelsb2 30986 cvrcmp 32920 cvlatexch3 32975 cvlsupr2 32980 atexchcvrN 33076 3dim1 33103 3dim2 33104 ps-1 33113 ps-2 33114 3atlem3 33121 3atlem5 33123 lplnnle2at 33177 lplnllnneN 33192 2llnjaN 33202 4atlem3 33232 4atlem10b 33241 4atlem12 33248 2llnma3r 33424 paddasslem4 33459 paddasslem7 33462 paddasslem8 33463 paddasslem12 33467 paddasslem13 33468 pmodlem1 33482 pmodlem2 33483 llnexchb2lem 33504 4atex2 33713 ltrnatlw 33820 trlval4 33825 arglem1N 33827 cdlemd4 33838 cdlemd5 33839 cdleme0moN 33862 cdleme16 33922 cdleme20 33962 cdleme21j 33974 cdleme21k 33976 cdleme27N 34007 cdleme28c 34010 cdleme43fsv1snlem 34058 cdleme38n 34102 cdleme40n 34106 cdleme41snaw 34114 cdlemg6c 34258 cdlemg8c 34267 cdlemg8 34269 cdlemg12e 34285 cdlemg16 34295 cdlemg16ALTN 34296 cdlemg16z 34297 cdlemg16zz 34298 cdlemg18a 34316 cdlemg20 34323 cdlemg22 34325 cdlemg37 34327 cdlemg27b 34334 cdlemg31d 34338 cdlemg33 34349 cdlemg38 34353 cdlemg44b 34370 cdlemk38 34553 cdlemk35s-id 34576 cdlemk39s-id 34578 cdlemk55 34599 cdlemk35u 34602 cdlemk55u 34604 cdleml3N 34616 cdlemn11pre 34849 |
Copyright terms: Public domain | W3C validator |