Theorem simp22l 1305

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

Assertion

Ref	Expression
simp22l	⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)

Proof of Theorem simp22l

Step	Hyp	Ref	Expression
1		simp2l 1212	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1146	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ttrclselem2  9678  ax5seglem6  29081  segconeu  36325  3atlem2  40072  lplncvrlvol2  40203  paddasslem15  40422  4atex  40664  trlval4  40776  cdlemc5  40783  cdlemc6  40784  cdlemd2  40787  cdlemd3  40788  cdlemd4  40789  cdleme0moN  40813  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme11g  40853  cdleme11h  40854  cdleme11j  40855  cdleme11k  40856  cdleme11l  40857  cdleme11  40858  cdleme14  40861  cdleme15a  40862  cdleme15c  40864  cdleme15d  40865  cdleme15  40866  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme16e  40870  cdleme16f  40871  cdleme18a  40879  cdleme18b  40880  cdleme18c  40881  cdleme19b  40892  cdleme19e  40895  cdleme20bN  40898  cdleme20c  40899  cdleme20d  40900  cdleme20e  40901  cdleme20f  40902  cdleme20g  40903  cdleme20h  40904  cdleme20j  40906  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme21ct  40917  cdleme22d  40931  cdleme22e  40932  cdleme22eALTN  40933  cdleme26e  40947  cdleme27a  40955  cdleme28a  40958  cdleme30a  40966  cdleme43fsv1snlem  41008  cdlemefs44  41014  cdlemefs45ee  41018  cdleme35sn2aw  41046  cdleme36a  41048  cdleme39n  41054  cdleme40m  41055  cdleme42k  41072  cdlemeg47rv2  41098  cdlemeg46frv  41113  cdlemeg46vrg  41115  cdlemeg46rgv  41116  cdlemeg46req  41117  cdlemg2fv2  41188  cdlemg4g  41204  cdlemg4  41205  cdlemg6c  41208  cdlemg8b  41216  cdlemg8c  41217  cdlemg9a  41220  cdlemg9b  41221  cdlemg9  41222  cdlemg12a  41231  cdlemg12b  41232  cdlemg12c  41233  cdlemg17h  41256  cdlemg18b  41267  cdlemg18c  41268  cdlemg31b0a  41283  cdlemg27b  41284  cdlemg31d  41288  cdlemg28b  41291  cdlemg33a  41294  cdlemg33b  41295  cdlemg33c  41296  cdlemg33d  41297  cdlemg33e  41298  cdlemg33  41299  cdlemh  41405  cdlemk6  41425  cdlemki  41429  cdlemksat  41434  cdlemksv2  41435  cdlemk7  41436  cdlemk11  41437  cdlemk12  41438  cdlemkole  41441  cdlemk14  41442  cdlemk15  41443  cdlemk17  41446  cdlemk1u  41447  cdlemk5u  41449  cdlemk6u  41450  cdlemk7u  41458  cdlemk11u  41459  cdlemk12u  41460  cdlemk7u-2N  41476  cdlemk11u-2N  41477  cdlemk12u-2N  41478  cdlemk20-2N  41480  cdlemk28-3  41496  cdlemk33N  41497  cdlemk34  41498  cdlemk37  41502  cdlemk39  41504  cdlemk35s  41525  cdlemk39s  41527  cdlemk47  41537  cdlemk48  41538  cdlemk50  41540  cdlemk51  41541  cdlemk52  41542  cdlemkyyN  41550  cdlemk43N  41551  cdlemn2  41783  cdlemn10  41794