Theorem simp22l 1311

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

Assertion

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

Proof of Theorem simp22l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ttrclselem2  9709  ax5seglem6  29399  segconeu  36599  3atlem2  40365  lplncvrlvol2  40496  paddasslem15  40715  4atex  40957  trlval4  41069  cdlemc5  41076  cdlemc6  41077  cdlemd2  41080  cdlemd3  41081  cdlemd4  41082  cdleme0moN  41106  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme11g  41146  cdleme11h  41147  cdleme11j  41148  cdleme11k  41149  cdleme11l  41150  cdleme11  41151  cdleme14  41154  cdleme15a  41155  cdleme15c  41157  cdleme15d  41158  cdleme15  41159  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme16e  41163  cdleme16f  41164  cdleme18a  41172  cdleme18b  41173  cdleme18c  41174  cdleme19b  41185  cdleme19e  41188  cdleme20bN  41191  cdleme20c  41192  cdleme20d  41193  cdleme20e  41194  cdleme20f  41195  cdleme20g  41196  cdleme20h  41197  cdleme20j  41199  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme21ct  41210  cdleme22d  41224  cdleme22e  41225  cdleme22eALTN  41226  cdleme26e  41240  cdleme27a  41248  cdleme28a  41251  cdleme30a  41259  cdleme43fsv1snlem  41301  cdlemefs44  41307  cdlemefs45ee  41311  cdleme35sn2aw  41339  cdleme36a  41341  cdleme39n  41347  cdleme40m  41348  cdleme42k  41365  cdlemeg47rv2  41391  cdlemeg46frv  41406  cdlemeg46vrg  41408  cdlemeg46rgv  41409  cdlemeg46req  41410  cdlemg2fv2  41481  cdlemg4g  41497  cdlemg4  41498  cdlemg6c  41501  cdlemg8b  41509  cdlemg8c  41510  cdlemg9a  41513  cdlemg9b  41514  cdlemg9  41515  cdlemg12a  41524  cdlemg12b  41525  cdlemg12c  41526  cdlemg17h  41549  cdlemg18b  41560  cdlemg18c  41561  cdlemg31b0a  41576  cdlemg27b  41577  cdlemg31d  41581  cdlemg28b  41584  cdlemg33a  41587  cdlemg33b  41588  cdlemg33c  41589  cdlemg33d  41590  cdlemg33e  41591  cdlemg33  41592  cdlemh  41698  cdlemk6  41718  cdlemki  41722  cdlemksat  41727  cdlemksv2  41728  cdlemk7  41729  cdlemk11  41730  cdlemk12  41731  cdlemkole  41734  cdlemk14  41735  cdlemk15  41736  cdlemk17  41739  cdlemk1u  41740  cdlemk5u  41742  cdlemk6u  41743  cdlemk7u  41751  cdlemk11u  41752  cdlemk12u  41753  cdlemk7u-2N  41769  cdlemk11u-2N  41770  cdlemk12u-2N  41771  cdlemk20-2N  41773  cdlemk28-3  41789  cdlemk33N  41790  cdlemk34  41791  cdlemk37  41795  cdlemk39  41797  cdlemk35s  41818  cdlemk39s  41820  cdlemk47  41830  cdlemk48  41831  cdlemk50  41833  cdlemk51  41834  cdlemk52  41835  cdlemkyyN  41843  cdlemk43N  41844  cdlemn2  42076  cdlemn10  42087