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 1135	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  modexp  14201  segconeu  34983  4atlem10  38477  lplncvrlvol2  38486  4atex  38947  4atex2-0cOLDN  38951  cdlemd2  39070  cdlemd3  39071  cdlemd4  39072  cdleme0e  39088  cdleme0moN  39096  cdleme3g  39105  cdleme3h  39106  cdleme3  39108  cdleme9  39124  cdleme11c  39132  cdleme11dN  39133  cdleme11e  39134  cdleme11fN  39135  cdleme11h  39137  cdleme11j  39138  cdleme11k  39139  cdleme11  39141  cdleme12  39142  cdleme13  39143  cdleme14  39144  cdleme15a  39145  cdleme15b  39146  cdleme15c  39147  cdleme15d  39148  cdleme15  39149  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme16e  39153  cdleme16f  39154  cdleme17d1  39160  cdleme18a  39162  cdleme18b  39163  cdleme18c  39164  cdleme18d  39166  cdleme19b  39175  cdleme19d  39177  cdleme19e  39178  cdleme20c  39182  cdleme20d  39183  cdleme20e  39184  cdleme20f  39185  cdleme20g  39186  cdleme20h  39187  cdleme20j  39189  cdleme20l2  39192  cdleme20l  39193  cdleme20m  39194  cdleme20  39195  cdleme21ct  39200  cdleme21e  39202  cdleme21i  39206  cdleme22aa  39210  cdleme22cN  39213  cdleme22d  39214  cdleme22e  39215  cdleme22eALTN  39216  cdleme22f  39217  cdleme26e  39230  cdleme27a  39238  cdleme32e  39316  cdlemg2fv2  39471  cdlemg4a  39479  cdlemg4d  39484  cdlemg4  39488  cdlemg6c  39491  cdlemg8b  39499  cdlemg8c  39500  cdlemg9a  39503  cdlemg9  39505  cdlemg12a  39514  cdlemg12c  39516  cdlemg17dALTN  39535  cdlemg17h  39539  cdlemg18b  39550  cdlemg18c  39551  cdlemg18d  39552  cdlemg18  39553  cdlemg19a  39554  cdlemg21  39557  cdlemg28a  39564  cdlemg31b0a  39566  cdlemg31d  39571  cdlemg33b0  39572  cdlemg33a  39577  cdlemh  39688  cdlemk5  39707  cdlemk6  39708  cdlemk7  39719  cdlemk11  39720  cdlemk12  39721  cdlemk21N  39744  cdlemk20  39745  cdlemk28-3  39779  cdlemk34  39781  cdlemkfid3N  39796  cdlemk35s-id  39809  cdlemk39s-id  39811  cdlemk55u1  39836  cdlemn2  40066  cdlemn10  40077  dihjustlem  40087