Theorem simp22l 1115

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

Assertion

Ref	Expression
simp22l

Proof of Theorem simp22l

Step	Hyp	Ref	Expression
1		simp2l 1022	. 2
2	1	3ad2ant2 1018	1

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

This theorem is referenced by:  ax5seglem6  24237  segconeu  29661  3atlem2  35208  lplncvrlvol2  35339  paddasslem15  35558  4atex  35800  trlval4  35913  cdlemc5  35920  cdlemc6  35921  cdlemd2  35924  cdlemd3  35925  cdlemd4  35926  cdleme0moN  35950  cdleme3g  35959  cdleme3h  35960  cdleme3  35962  cdleme11g  35990  cdleme11h  35991  cdleme11j  35992  cdleme11k  35993  cdleme11l  35994  cdleme11  35995  cdleme14  35998  cdleme15a  35999  cdleme15c  36001  cdleme15d  36002  cdleme15  36003  cdleme16b  36004  cdleme16c  36005  cdleme16d  36006  cdleme16e  36007  cdleme16f  36008  cdleme18a  36016  cdleme18b  36017  cdleme18c  36018  cdleme19b  36030  cdleme19e  36033  cdleme20bN  36036  cdleme20c  36037  cdleme20d  36038  cdleme20e  36039  cdleme20f  36040  cdleme20g  36041  cdleme20h  36042  cdleme20j  36044  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme21ct  36055  cdleme22d  36069  cdleme22e  36070  cdleme22eALTN  36071  cdleme26e  36085  cdleme27a  36093  cdleme28a  36096  cdleme30a  36104  cdleme43fsv1snlem  36146  cdlemefs44  36152  cdlemefs45ee  36156  cdleme35sn2aw  36184  cdleme36a  36186  cdleme39n  36192  cdleme40m  36193  cdleme42k  36210  cdlemeg47rv2  36236  cdlemeg46frv  36251  cdlemeg46vrg  36253  cdlemeg46rgv  36254  cdlemeg46req  36255  cdlemg2fv2  36326  cdlemg4g  36342  cdlemg4  36343  cdlemg6c  36346  cdlemg8b  36354  cdlemg8c  36355  cdlemg9a  36358  cdlemg9b  36359  cdlemg9  36360  cdlemg12a  36369  cdlemg12b  36370  cdlemg12c  36371  cdlemg17h  36394  cdlemg18b  36405  cdlemg18c  36406  cdlemg31b0a  36421  cdlemg27b  36422  cdlemg31d  36426  cdlemg28b  36429  cdlemg33a  36432  cdlemg33b  36433  cdlemg33c  36434  cdlemg33d  36435  cdlemg33e  36436  cdlemg33  36437  cdlemh  36543  cdlemk6  36563  cdlemki  36567  cdlemksat  36572  cdlemksv2  36573  cdlemk7  36574  cdlemk11  36575  cdlemk12  36576  cdlemkole  36579  cdlemk14  36580  cdlemk15  36581  cdlemk17  36584  cdlemk1u  36585  cdlemk5u  36587  cdlemk6u  36588  cdlemk7u  36596  cdlemk11u  36597  cdlemk12u  36598  cdlemk7u-2N  36614  cdlemk11u-2N  36615  cdlemk12u-2N  36616  cdlemk20-2N  36618  cdlemk28-3  36634  cdlemk33N  36635  cdlemk34  36636  cdlemk37  36640  cdlemk39  36642  cdlemk35s  36663  cdlemk39s  36665  cdlemk47  36675  cdlemk48  36676  cdlemk50  36678  cdlemk51  36679  cdlemk52  36680  cdlemkyyN  36688  cdlemk43N  36689  cdlemn2  36922  cdlemn10  36933

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