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  9705  ax5seglem6  29321  segconeu  36524  3atlem2  40299  lplncvrlvol2  40430  paddasslem15  40649  4atex  40891  trlval4  41003  cdlemc5  41010  cdlemc6  41011  cdlemd2  41014  cdlemd3  41015  cdlemd4  41016  cdleme0moN  41040  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme11g  41080  cdleme11h  41081  cdleme11j  41082  cdleme11k  41083  cdleme11l  41084  cdleme11  41085  cdleme14  41088  cdleme15a  41089  cdleme15c  41091  cdleme15d  41092  cdleme15  41093  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme16e  41097  cdleme16f  41098  cdleme18a  41106  cdleme18b  41107  cdleme18c  41108  cdleme19b  41119  cdleme19e  41122  cdleme20bN  41125  cdleme20c  41126  cdleme20d  41127  cdleme20e  41128  cdleme20f  41129  cdleme20g  41130  cdleme20h  41131  cdleme20j  41133  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme21ct  41144  cdleme22d  41158  cdleme22e  41159  cdleme22eALTN  41160  cdleme26e  41174  cdleme27a  41182  cdleme28a  41185  cdleme30a  41193  cdleme43fsv1snlem  41235  cdlemefs44  41241  cdlemefs45ee  41245  cdleme35sn2aw  41273  cdleme36a  41275  cdleme39n  41281  cdleme40m  41282  cdleme42k  41299  cdlemeg47rv2  41325  cdlemeg46frv  41340  cdlemeg46vrg  41342  cdlemeg46rgv  41343  cdlemeg46req  41344  cdlemg2fv2  41415  cdlemg4g  41431  cdlemg4  41432  cdlemg6c  41435  cdlemg8b  41443  cdlemg8c  41444  cdlemg9a  41447  cdlemg9b  41448  cdlemg9  41449  cdlemg12a  41458  cdlemg12b  41459  cdlemg12c  41460  cdlemg17h  41483  cdlemg18b  41494  cdlemg18c  41495  cdlemg31b0a  41510  cdlemg27b  41511  cdlemg31d  41515  cdlemg28b  41518  cdlemg33a  41521  cdlemg33b  41522  cdlemg33c  41523  cdlemg33d  41524  cdlemg33e  41525  cdlemg33  41526  cdlemh  41632  cdlemk6  41652  cdlemki  41656  cdlemksat  41661  cdlemksv2  41662  cdlemk7  41663  cdlemk11  41664  cdlemk12  41665  cdlemkole  41668  cdlemk14  41669  cdlemk15  41670  cdlemk17  41673  cdlemk1u  41674  cdlemk5u  41676  cdlemk6u  41677  cdlemk7u  41685  cdlemk11u  41686  cdlemk12u  41687  cdlemk7u-2N  41703  cdlemk11u-2N  41704  cdlemk12u-2N  41705  cdlemk20-2N  41707  cdlemk28-3  41723  cdlemk33N  41724  cdlemk34  41725  cdlemk37  41729  cdlemk39  41731  cdlemk35s  41752  cdlemk39s  41754  cdlemk47  41764  cdlemk48  41765  cdlemk50  41767  cdlemk51  41768  cdlemk52  41769  cdlemkyyN  41777  cdlemk43N  41778  cdlemn2  42010  cdlemn10  42021