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  14198  segconeu  34972  4atlem10  38466  lplncvrlvol2  38475  4atex  38936  4atex2-0cOLDN  38940  cdlemd2  39059  cdlemd3  39060  cdlemd4  39061  cdleme0e  39077  cdleme0moN  39085  cdleme3g  39094  cdleme3h  39095  cdleme3  39097  cdleme9  39113  cdleme11c  39121  cdleme11dN  39122  cdleme11e  39123  cdleme11fN  39124  cdleme11h  39126  cdleme11j  39127  cdleme11k  39128  cdleme11  39130  cdleme12  39131  cdleme13  39132  cdleme14  39133  cdleme15a  39134  cdleme15b  39135  cdleme15c  39136  cdleme15d  39137  cdleme15  39138  cdleme16b  39139  cdleme16c  39140  cdleme16d  39141  cdleme16e  39142  cdleme16f  39143  cdleme17d1  39149  cdleme18a  39151  cdleme18b  39152  cdleme18c  39153  cdleme18d  39155  cdleme19b  39164  cdleme19d  39166  cdleme19e  39167  cdleme20c  39171  cdleme20d  39172  cdleme20e  39173  cdleme20f  39174  cdleme20g  39175  cdleme20h  39176  cdleme20j  39178  cdleme20l2  39181  cdleme20l  39182  cdleme20m  39183  cdleme20  39184  cdleme21ct  39189  cdleme21e  39191  cdleme21i  39195  cdleme22aa  39199  cdleme22cN  39202  cdleme22d  39203  cdleme22e  39204  cdleme22eALTN  39205  cdleme22f  39206  cdleme26e  39219  cdleme27a  39227  cdleme32e  39305  cdlemg2fv2  39460  cdlemg4a  39468  cdlemg4d  39473  cdlemg4  39477  cdlemg6c  39480  cdlemg8b  39488  cdlemg8c  39489  cdlemg9a  39492  cdlemg9  39494  cdlemg12a  39503  cdlemg12c  39505  cdlemg17dALTN  39524  cdlemg17h  39528  cdlemg18b  39539  cdlemg18c  39540  cdlemg18d  39541  cdlemg18  39542  cdlemg19a  39543  cdlemg21  39546  cdlemg28a  39553  cdlemg31b0a  39555  cdlemg31d  39560  cdlemg33b0  39561  cdlemg33a  39566  cdlemh  39677  cdlemk5  39696  cdlemk6  39697  cdlemk7  39708  cdlemk11  39709  cdlemk12  39710  cdlemk21N  39733  cdlemk20  39734  cdlemk28-3  39768  cdlemk34  39770  cdlemkfid3N  39785  cdlemk35s-id  39798  cdlemk39s-id  39800  cdlemk55u1  39825  cdlemn2  40055  cdlemn10  40066  dihjustlem  40076