Theorem simp23r 1118

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp23r

Proof of Theorem simp23r

Step	Hyp	Ref	Expression
1		simp3r 1025	. 2
2	1	3ad2ant2 1018	1

Syntax hints:  ->wi 4  /\wa 369  /\w3a 973

This theorem is referenced by:  ax5seglem6  24237  lshpkrlem5  34839  lplnexllnN  35288  4atexlemutvt  35778  cdlemc5  35920  cdlemd2  35924  cdleme0moN  35950  cdleme3h  35960  cdleme5  35965  cdleme9  35978  cdleme11l  35994  cdleme14  35998  cdleme15c  36001  cdleme16b  36004  cdleme16d  36006  cdleme16e  36007  cdlemednpq  36024  cdleme20bN  36036  cdleme20j  36044  cdleme20l2  36047  cdleme20l  36048  cdleme22cN  36068  cdleme22d  36069  cdleme22e  36070  cdleme22f  36072  cdleme26fALTN  36088  cdleme26f  36089  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme27a  36093  cdleme32b  36168  cdleme32d  36170  cdleme32f  36172  cdleme39n  36192  cdleme40n  36194  cdlemg2fv2  36326  cdlemg17h  36394  cdlemg27b  36422  cdlemg28b  36429  cdlemg28  36430  cdlemg29  36431  cdlemg33a  36432  cdlemg33d  36435  cdlemk7u-2N  36614  cdlemk11u-2N  36615  cdlemk12u-2N  36616  cdlemk26-3  36632  cdlemk27-3  36633  cdlemkfid3N  36651  cdlemn11c  36936

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 185  df-an 371  df-3an 975