Theorem simp21l 1290

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1197	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1134	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  modexp  14287  segconeu  35975  4atlem10  39563  lplncvrlvol2  39572  4atex  40033  4atex2-0cOLDN  40037  cdlemd2  40156  cdlemd3  40157  cdlemd4  40158  cdleme0e  40174  cdleme0moN  40182  cdleme3g  40191  cdleme3h  40192  cdleme3  40194  cdleme9  40210  cdleme11c  40218  cdleme11dN  40219  cdleme11e  40220  cdleme11fN  40221  cdleme11h  40223  cdleme11j  40224  cdleme11k  40225  cdleme11  40227  cdleme12  40228  cdleme13  40229  cdleme14  40230  cdleme15a  40231  cdleme15b  40232  cdleme15c  40233  cdleme15d  40234  cdleme15  40235  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme16f  40240  cdleme17d1  40246  cdleme18a  40248  cdleme18b  40249  cdleme18c  40250  cdleme18d  40252  cdleme19b  40261  cdleme19d  40263  cdleme19e  40264  cdleme20c  40268  cdleme20d  40269  cdleme20e  40270  cdleme20f  40271  cdleme20g  40272  cdleme20h  40273  cdleme20j  40275  cdleme20l2  40278  cdleme20l  40279  cdleme20m  40280  cdleme20  40281  cdleme21ct  40286  cdleme21e  40288  cdleme21i  40292  cdleme22aa  40296  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme22f  40303  cdleme26e  40316  cdleme27a  40324  cdleme32e  40402  cdlemg2fv2  40557  cdlemg4a  40565  cdlemg4d  40570  cdlemg4  40574  cdlemg6c  40577  cdlemg8b  40585  cdlemg8c  40586  cdlemg9a  40589  cdlemg9  40591  cdlemg12a  40600  cdlemg12c  40602  cdlemg17dALTN  40621  cdlemg17h  40625  cdlemg18b  40636  cdlemg18c  40637  cdlemg18d  40638  cdlemg18  40639  cdlemg19a  40640  cdlemg21  40643  cdlemg28a  40650  cdlemg31b0a  40652  cdlemg31d  40657  cdlemg33b0  40658  cdlemg33a  40663  cdlemh  40774  cdlemk5  40793  cdlemk6  40794  cdlemk7  40805  cdlemk11  40806  cdlemk12  40807  cdlemk21N  40830  cdlemk20  40831  cdlemk28-3  40865  cdlemk34  40867  cdlemkfid3N  40882  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk55u1  40922  cdlemn2  41152  cdlemn10  41163  dihjustlem  41173