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  14256  segconeu  36029  4atlem10  39625  lplncvrlvol2  39634  4atex  40095  4atex2-0cOLDN  40099  cdlemd2  40218  cdlemd3  40219  cdlemd4  40220  cdleme0e  40236  cdleme0moN  40244  cdleme3g  40253  cdleme3h  40254  cdleme3  40256  cdleme9  40272  cdleme11c  40280  cdleme11dN  40281  cdleme11e  40282  cdleme11fN  40283  cdleme11h  40285  cdleme11j  40286  cdleme11k  40287  cdleme11  40289  cdleme12  40290  cdleme13  40291  cdleme14  40292  cdleme15a  40293  cdleme15b  40294  cdleme15c  40295  cdleme15d  40296  cdleme15  40297  cdleme16b  40298  cdleme16c  40299  cdleme16d  40300  cdleme16e  40301  cdleme16f  40302  cdleme17d1  40308  cdleme18a  40310  cdleme18b  40311  cdleme18c  40312  cdleme18d  40314  cdleme19b  40323  cdleme19d  40325  cdleme19e  40326  cdleme20c  40330  cdleme20d  40331  cdleme20e  40332  cdleme20f  40333  cdleme20g  40334  cdleme20h  40335  cdleme20j  40337  cdleme20l2  40340  cdleme20l  40341  cdleme20m  40342  cdleme20  40343  cdleme21ct  40348  cdleme21e  40350  cdleme21i  40354  cdleme22aa  40358  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22eALTN  40364  cdleme22f  40365  cdleme26e  40378  cdleme27a  40386  cdleme32e  40464  cdlemg2fv2  40619  cdlemg4a  40627  cdlemg4d  40632  cdlemg4  40636  cdlemg6c  40639  cdlemg8b  40647  cdlemg8c  40648  cdlemg9a  40651  cdlemg9  40653  cdlemg12a  40662  cdlemg12c  40664  cdlemg17dALTN  40683  cdlemg17h  40687  cdlemg18b  40698  cdlemg18c  40699  cdlemg18d  40700  cdlemg18  40701  cdlemg19a  40702  cdlemg21  40705  cdlemg28a  40712  cdlemg31b0a  40714  cdlemg31d  40719  cdlemg33b0  40720  cdlemg33a  40725  cdlemh  40836  cdlemk5  40855  cdlemk6  40856  cdlemk7  40867  cdlemk11  40868  cdlemk12  40869  cdlemk21N  40892  cdlemk20  40893  cdlemk28-3  40927  cdlemk34  40929  cdlemkfid3N  40944  cdlemk35s-id  40957  cdlemk39s-id  40959  cdlemk55u1  40984  cdlemn2  41214  cdlemn10  41225  dihjustlem  41235