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  35014  4atlem10  38525  lplncvrlvol2  38534  4atex  38995  4atex2-0cOLDN  38999  cdlemd2  39118  cdlemd3  39119  cdlemd4  39120  cdleme0e  39136  cdleme0moN  39144  cdleme3g  39153  cdleme3h  39154  cdleme3  39156  cdleme9  39172  cdleme11c  39180  cdleme11dN  39181  cdleme11e  39182  cdleme11fN  39183  cdleme11h  39185  cdleme11j  39186  cdleme11k  39187  cdleme11  39189  cdleme12  39190  cdleme13  39191  cdleme14  39192  cdleme15a  39193  cdleme15b  39194  cdleme15c  39195  cdleme15d  39196  cdleme15  39197  cdleme16b  39198  cdleme16c  39199  cdleme16d  39200  cdleme16e  39201  cdleme16f  39202  cdleme17d1  39208  cdleme18a  39210  cdleme18b  39211  cdleme18c  39212  cdleme18d  39214  cdleme19b  39223  cdleme19d  39225  cdleme19e  39226  cdleme20c  39230  cdleme20d  39231  cdleme20e  39232  cdleme20f  39233  cdleme20g  39234  cdleme20h  39235  cdleme20j  39237  cdleme20l2  39240  cdleme20l  39241  cdleme20m  39242  cdleme20  39243  cdleme21ct  39248  cdleme21e  39250  cdleme21i  39254  cdleme22aa  39258  cdleme22cN  39261  cdleme22d  39262  cdleme22e  39263  cdleme22eALTN  39264  cdleme22f  39265  cdleme26e  39278  cdleme27a  39286  cdleme32e  39364  cdlemg2fv2  39519  cdlemg4a  39527  cdlemg4d  39532  cdlemg4  39536  cdlemg6c  39539  cdlemg8b  39547  cdlemg8c  39548  cdlemg9a  39551  cdlemg9  39553  cdlemg12a  39562  cdlemg12c  39564  cdlemg17dALTN  39583  cdlemg17h  39587  cdlemg18b  39598  cdlemg18c  39599  cdlemg18d  39600  cdlemg18  39601  cdlemg19a  39602  cdlemg21  39605  cdlemg28a  39612  cdlemg31b0a  39614  cdlemg31d  39619  cdlemg33b0  39620  cdlemg33a  39625  cdlemh  39736  cdlemk5  39755  cdlemk6  39756  cdlemk7  39767  cdlemk11  39768  cdlemk12  39769  cdlemk21N  39792  cdlemk20  39793  cdlemk28-3  39827  cdlemk34  39829  cdlemkfid3N  39844  cdlemk35s-id  39857  cdlemk39s-id  39859  cdlemk55u1  39884  cdlemn2  40114  cdlemn10  40125  dihjustlem  40135