Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simp23r | Structured version Visualization version Unicode version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
Ref | Expression |
---|---|
simp23r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3r 1090 | . 2 | |
2 | 1 | 3ad2ant2 1083 | 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: ax5seglem6 25814 lshpkrlem5 34401 lplnexllnN 34850 4atexlemutvt 35340 cdlemc5 35482 cdlemd2 35486 cdleme0moN 35512 cdleme3h 35522 cdleme5 35527 cdleme9 35540 cdleme11l 35556 cdleme14 35560 cdleme15c 35563 cdleme16b 35566 cdleme16d 35568 cdleme16e 35569 cdlemednpq 35586 cdleme20bN 35598 cdleme20j 35606 cdleme20l2 35609 cdleme20l 35610 cdleme22cN 35630 cdleme22d 35631 cdleme22e 35632 cdleme22f 35634 cdleme26fALTN 35650 cdleme26f 35651 cdleme26f2ALTN 35652 cdleme26f2 35653 cdleme27a 35655 cdleme32b 35730 cdleme32d 35732 cdleme32f 35734 cdleme39n 35754 cdleme40n 35756 cdlemg2fv2 35888 cdlemg17h 35956 cdlemg27b 35984 cdlemg28b 35991 cdlemg28 35992 cdlemg29 35993 cdlemg33a 35994 cdlemg33d 35997 cdlemk7u-2N 36176 cdlemk11u-2N 36177 cdlemk12u-2N 36178 cdlemk26-3 36194 cdlemk27-3 36195 cdlemkfid3N 36213 cdlemn11c 36498 |
Copyright terms: Public domain | W3C validator |