Theorem simp21l 1291

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1198	. 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:  modexp  14203  segconeu  35999  4atlem10  39600  lplncvrlvol2  39609  4atex  40070  4atex2-0cOLDN  40074  cdlemd2  40193  cdlemd3  40194  cdlemd4  40195  cdleme0e  40211  cdleme0moN  40219  cdleme3g  40228  cdleme3h  40229  cdleme3  40231  cdleme9  40247  cdleme11c  40255  cdleme11dN  40256  cdleme11e  40257  cdleme11fN  40258  cdleme11h  40260  cdleme11j  40261  cdleme11k  40262  cdleme11  40264  cdleme12  40265  cdleme13  40266  cdleme14  40267  cdleme15a  40268  cdleme15b  40269  cdleme15c  40270  cdleme15d  40271  cdleme15  40272  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme16f  40277  cdleme17d1  40283  cdleme18a  40285  cdleme18b  40286  cdleme18c  40287  cdleme18d  40289  cdleme19b  40298  cdleme19d  40300  cdleme19e  40301  cdleme20c  40305  cdleme20d  40306  cdleme20e  40307  cdleme20f  40308  cdleme20g  40309  cdleme20h  40310  cdleme20j  40312  cdleme20l2  40315  cdleme20l  40316  cdleme20m  40317  cdleme20  40318  cdleme21ct  40323  cdleme21e  40325  cdleme21i  40329  cdleme22aa  40333  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme22f  40340  cdleme26e  40353  cdleme27a  40361  cdleme32e  40439  cdlemg2fv2  40594  cdlemg4a  40602  cdlemg4d  40607  cdlemg4  40611  cdlemg6c  40614  cdlemg8b  40622  cdlemg8c  40623  cdlemg9a  40626  cdlemg9  40628  cdlemg12a  40637  cdlemg12c  40639  cdlemg17dALTN  40658  cdlemg17h  40662  cdlemg18b  40673  cdlemg18c  40674  cdlemg18d  40675  cdlemg18  40676  cdlemg19a  40677  cdlemg21  40680  cdlemg28a  40687  cdlemg31b0a  40689  cdlemg31d  40694  cdlemg33b0  40695  cdlemg33a  40700  cdlemh  40811  cdlemk5  40830  cdlemk6  40831  cdlemk7  40842  cdlemk11  40843  cdlemk12  40844  cdlemk21N  40867  cdlemk20  40868  cdlemk28-3  40902  cdlemk34  40904  cdlemkfid3N  40919  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk55u1  40959  cdlemn2  41189  cdlemn10  41200  dihjustlem  41210