Theorem simp22l 1292

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

Assertion

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

Proof of Theorem simp22l

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

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ttrclselem2  9795  ax5seglem6  28967  segconeu  35975  3atlem2  39441  lplncvrlvol2  39572  paddasslem15  39791  4atex  40033  trlval4  40145  cdlemc5  40152  cdlemc6  40153  cdlemd2  40156  cdlemd3  40157  cdlemd4  40158  cdleme0moN  40182  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme11g  40222  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme11l  40226  cdleme11  40227  cdleme14  40230  cdleme15a  40231  cdleme15c  40233  cdleme15d  40234  cdleme15  40235  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme18a  40248  cdleme18b  40249  cdleme18c  40250  cdleme19b  40261  cdleme19e  40264  cdleme20bN  40267  cdleme20c  40268  cdleme20d  40269  cdleme20e  40270  cdleme20f  40271  cdleme20g  40272  cdleme20h  40273  cdleme20j  40275  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme21ct  40286  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme26e  40316  cdleme27a  40324  cdleme28a  40327  cdleme30a  40335  cdleme43fsv1snlem  40377  cdlemefs44  40383  cdlemefs45ee  40387  cdleme35sn2aw  40415  cdleme36a  40417  cdleme39n  40423  cdleme40m  40424  cdleme42k  40441  cdlemeg47rv2  40467  cdlemeg46frv  40482  cdlemeg46vrg  40484  cdlemeg46rgv  40485  cdlemeg46req  40486  cdlemg2fv2  40557  cdlemg4g  40573  cdlemg4  40574  cdlemg6c  40577  cdlemg8b  40585  cdlemg8c  40586  cdlemg9a  40589  cdlemg9b  40590  cdlemg9  40591  cdlemg12a  40600  cdlemg12b  40601  cdlemg12c  40602  cdlemg17h  40625  cdlemg18b  40636  cdlemg18c  40637  cdlemg31b0a  40652  cdlemg27b  40653  cdlemg31d  40657  cdlemg28b  40660  cdlemg33a  40663  cdlemg33b  40664  cdlemg33c  40665  cdlemg33d  40666  cdlemg33e  40667  cdlemg33  40668  cdlemh  40774  cdlemk6  40794  cdlemki  40798  cdlemksat  40803  cdlemksv2  40804  cdlemk7  40805  cdlemk11  40806  cdlemk12  40807  cdlemkole  40810  cdlemk14  40811  cdlemk15  40812  cdlemk17  40815  cdlemk1u  40816  cdlemk5u  40818  cdlemk6u  40819  cdlemk7u  40827  cdlemk11u  40828  cdlemk12u  40829  cdlemk7u-2N  40845  cdlemk11u-2N  40846  cdlemk12u-2N  40847  cdlemk20-2N  40849  cdlemk28-3  40865  cdlemk33N  40866  cdlemk34  40867  cdlemk37  40871  cdlemk39  40873  cdlemk35s  40894  cdlemk39s  40896  cdlemk47  40906  cdlemk48  40907  cdlemk50  40909  cdlemk51  40910  cdlemk52  40911  cdlemkyyN  40919  cdlemk43N  40920  cdlemn2  41152  cdlemn10  41163