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 400   ∧ 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 401  df-3an 1105

This theorem is used by:  ttrclselem2  9691  ax5seglem6  29293  segconeu  36511  3atlem2  40286  lplncvrlvol2  40417  paddasslem15  40636  4atex  40878  trlval4  40990  cdlemc5  40997  cdlemc6  40998  cdlemd2  41001  cdlemd3  41002  cdlemd4  41003  cdleme0moN  41027  cdleme3g  41036  cdleme3h  41037  cdleme3  41039  cdleme11g  41067  cdleme11h  41068  cdleme11j  41069  cdleme11k  41070  cdleme11l  41071  cdleme11  41072  cdleme14  41075  cdleme15a  41076  cdleme15c  41078  cdleme15d  41079  cdleme15  41080  cdleme16b  41081  cdleme16c  41082  cdleme16d  41083  cdleme16e  41084  cdleme16f  41085  cdleme18a  41093  cdleme18b  41094  cdleme18c  41095  cdleme19b  41106  cdleme19e  41109  cdleme20bN  41112  cdleme20c  41113  cdleme20d  41114  cdleme20e  41115  cdleme20f  41116  cdleme20g  41117  cdleme20h  41118  cdleme20j  41120  cdleme20l2  41123  cdleme20l  41124  cdleme20m  41125  cdleme21ct  41131  cdleme22d  41145  cdleme22e  41146  cdleme22eALTN  41147  cdleme26e  41161  cdleme27a  41169  cdleme28a  41172  cdleme30a  41180  cdleme43fsv1snlem  41222  cdlemefs44  41228  cdlemefs45ee  41232  cdleme35sn2aw  41260  cdleme36a  41262  cdleme39n  41268  cdleme40m  41269  cdleme42k  41286  cdlemeg47rv2  41312  cdlemeg46frv  41327  cdlemeg46vrg  41329  cdlemeg46rgv  41330  cdlemeg46req  41331  cdlemg2fv2  41402  cdlemg4g  41418  cdlemg4  41419  cdlemg6c  41422  cdlemg8b  41430  cdlemg8c  41431  cdlemg9a  41434  cdlemg9b  41435  cdlemg9  41436  cdlemg12a  41445  cdlemg12b  41446  cdlemg12c  41447  cdlemg17h  41470  cdlemg18b  41481  cdlemg18c  41482  cdlemg31b0a  41497  cdlemg27b  41498  cdlemg31d  41502  cdlemg28b  41505  cdlemg33a  41508  cdlemg33b  41509  cdlemg33c  41510  cdlemg33d  41511  cdlemg33e  41512  cdlemg33  41513  cdlemh  41619  cdlemk6  41639  cdlemki  41643  cdlemksat  41648  cdlemksv2  41649  cdlemk7  41650  cdlemk11  41651  cdlemk12  41652  cdlemkole  41655  cdlemk14  41656  cdlemk15  41657  cdlemk17  41660  cdlemk1u  41661  cdlemk5u  41663  cdlemk6u  41664  cdlemk7u  41672  cdlemk11u  41673  cdlemk12u  41674  cdlemk7u-2N  41690  cdlemk11u-2N  41691  cdlemk12u-2N  41692  cdlemk20-2N  41694  cdlemk28-3  41710  cdlemk33N  41711  cdlemk34  41712  cdlemk37  41716  cdlemk39  41718  cdlemk35s  41739  cdlemk39s  41741  cdlemk47  41751  cdlemk48  41752  cdlemk50  41754  cdlemk51  41755  cdlemk52  41756  cdlemkyyN  41764  cdlemk43N  41765  cdlemn2  41997  cdlemn10  42008