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 1086

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 1088

This theorem is referenced by:  ttrclselem2  9767  ax5seglem6  28950  segconeu  36013  3atlem2  39487  lplncvrlvol2  39618  paddasslem15  39837  4atex  40079  trlval4  40191  cdlemc5  40198  cdlemc6  40199  cdlemd2  40202  cdlemd3  40203  cdlemd4  40204  cdleme0moN  40228  cdleme3g  40237  cdleme3h  40238  cdleme3  40240  cdleme11g  40268  cdleme11h  40269  cdleme11j  40270  cdleme11k  40271  cdleme11l  40272  cdleme11  40273  cdleme14  40276  cdleme15a  40277  cdleme15c  40279  cdleme15d  40280  cdleme15  40281  cdleme16b  40282  cdleme16c  40283  cdleme16d  40284  cdleme16e  40285  cdleme16f  40286  cdleme18a  40294  cdleme18b  40295  cdleme18c  40296  cdleme19b  40307  cdleme19e  40310  cdleme20bN  40313  cdleme20c  40314  cdleme20d  40315  cdleme20e  40316  cdleme20f  40317  cdleme20g  40318  cdleme20h  40319  cdleme20j  40321  cdleme20l2  40324  cdleme20l  40325  cdleme20m  40326  cdleme21ct  40332  cdleme22d  40346  cdleme22e  40347  cdleme22eALTN  40348  cdleme26e  40362  cdleme27a  40370  cdleme28a  40373  cdleme30a  40381  cdleme43fsv1snlem  40423  cdlemefs44  40429  cdlemefs45ee  40433  cdleme35sn2aw  40461  cdleme36a  40463  cdleme39n  40469  cdleme40m  40470  cdleme42k  40487  cdlemeg47rv2  40513  cdlemeg46frv  40528  cdlemeg46vrg  40530  cdlemeg46rgv  40531  cdlemeg46req  40532  cdlemg2fv2  40603  cdlemg4g  40619  cdlemg4  40620  cdlemg6c  40623  cdlemg8b  40631  cdlemg8c  40632  cdlemg9a  40635  cdlemg9b  40636  cdlemg9  40637  cdlemg12a  40646  cdlemg12b  40647  cdlemg12c  40648  cdlemg17h  40671  cdlemg18b  40682  cdlemg18c  40683  cdlemg31b0a  40698  cdlemg27b  40699  cdlemg31d  40703  cdlemg28b  40706  cdlemg33a  40709  cdlemg33b  40710  cdlemg33c  40711  cdlemg33d  40712  cdlemg33e  40713  cdlemg33  40714  cdlemh  40820  cdlemk6  40840  cdlemki  40844  cdlemksat  40849  cdlemksv2  40850  cdlemk7  40851  cdlemk11  40852  cdlemk12  40853  cdlemkole  40856  cdlemk14  40857  cdlemk15  40858  cdlemk17  40861  cdlemk1u  40862  cdlemk5u  40864  cdlemk6u  40865  cdlemk7u  40873  cdlemk11u  40874  cdlemk12u  40875  cdlemk7u-2N  40891  cdlemk11u-2N  40892  cdlemk12u-2N  40893  cdlemk20-2N  40895  cdlemk28-3  40911  cdlemk33N  40912  cdlemk34  40913  cdlemk37  40917  cdlemk39  40919  cdlemk35s  40940  cdlemk39s  40942  cdlemk47  40952  cdlemk48  40953  cdlemk50  40955  cdlemk51  40956  cdlemk52  40957  cdlemkyyN  40965  cdlemk43N  40966  cdlemn2  41198  cdlemn10  41209