Theorem simp22l 1289

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

Assertion

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

Proof of Theorem simp22l

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084

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 206  df-an 396  df-3an 1086

This theorem is referenced by:  ttrclselem2  9716  ax5seglem6  28616  segconeu  35444  3atlem2  38811  lplncvrlvol2  38942  paddasslem15  39161  4atex  39403  trlval4  39515  cdlemc5  39522  cdlemc6  39523  cdlemd2  39526  cdlemd3  39527  cdlemd4  39528  cdleme0moN  39552  cdleme3g  39561  cdleme3h  39562  cdleme3  39564  cdleme11g  39592  cdleme11h  39593  cdleme11j  39594  cdleme11k  39595  cdleme11l  39596  cdleme11  39597  cdleme14  39600  cdleme15a  39601  cdleme15c  39603  cdleme15d  39604  cdleme15  39605  cdleme16b  39606  cdleme16c  39607  cdleme16d  39608  cdleme16e  39609  cdleme16f  39610  cdleme18a  39618  cdleme18b  39619  cdleme18c  39620  cdleme19b  39631  cdleme19e  39634  cdleme20bN  39637  cdleme20c  39638  cdleme20d  39639  cdleme20e  39640  cdleme20f  39641  cdleme20g  39642  cdleme20h  39643  cdleme20j  39645  cdleme20l2  39648  cdleme20l  39649  cdleme20m  39650  cdleme21ct  39656  cdleme22d  39670  cdleme22e  39671  cdleme22eALTN  39672  cdleme26e  39686  cdleme27a  39694  cdleme28a  39697  cdleme30a  39705  cdleme43fsv1snlem  39747  cdlemefs44  39753  cdlemefs45ee  39757  cdleme35sn2aw  39785  cdleme36a  39787  cdleme39n  39793  cdleme40m  39794  cdleme42k  39811  cdlemeg47rv2  39837  cdlemeg46frv  39852  cdlemeg46vrg  39854  cdlemeg46rgv  39855  cdlemeg46req  39856  cdlemg2fv2  39927  cdlemg4g  39943  cdlemg4  39944  cdlemg6c  39947  cdlemg8b  39955  cdlemg8c  39956  cdlemg9a  39959  cdlemg9b  39960  cdlemg9  39961  cdlemg12a  39970  cdlemg12b  39971  cdlemg12c  39972  cdlemg17h  39995  cdlemg18b  40006  cdlemg18c  40007  cdlemg31b0a  40022  cdlemg27b  40023  cdlemg31d  40027  cdlemg28b  40030  cdlemg33a  40033  cdlemg33b  40034  cdlemg33c  40035  cdlemg33d  40036  cdlemg33e  40037  cdlemg33  40038  cdlemh  40144  cdlemk6  40164  cdlemki  40168  cdlemksat  40173  cdlemksv2  40174  cdlemk7  40175  cdlemk11  40176  cdlemk12  40177  cdlemkole  40180  cdlemk14  40181  cdlemk15  40182  cdlemk17  40185  cdlemk1u  40186  cdlemk5u  40188  cdlemk6u  40189  cdlemk7u  40197  cdlemk11u  40198  cdlemk12u  40199  cdlemk7u-2N  40215  cdlemk11u-2N  40216  cdlemk12u-2N  40217  cdlemk20-2N  40219  cdlemk28-3  40235  cdlemk33N  40236  cdlemk34  40237  cdlemk37  40241  cdlemk39  40243  cdlemk35s  40264  cdlemk39s  40266  cdlemk47  40276  cdlemk48  40277  cdlemk50  40279  cdlemk51  40280  cdlemk52  40281  cdlemkyyN  40289  cdlemk43N  40290  cdlemn2  40522  cdlemn10  40533