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  14210  segconeu  36006  4atlem10  39607  lplncvrlvol2  39616  4atex  40077  4atex2-0cOLDN  40081  cdlemd2  40200  cdlemd3  40201  cdlemd4  40202  cdleme0e  40218  cdleme0moN  40226  cdleme3g  40235  cdleme3h  40236  cdleme3  40238  cdleme9  40254  cdleme11c  40262  cdleme11dN  40263  cdleme11e  40264  cdleme11fN  40265  cdleme11h  40267  cdleme11j  40268  cdleme11k  40269  cdleme11  40271  cdleme12  40272  cdleme13  40273  cdleme14  40274  cdleme15a  40275  cdleme15b  40276  cdleme15c  40277  cdleme15d  40278  cdleme15  40279  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme16f  40284  cdleme17d1  40290  cdleme18a  40292  cdleme18b  40293  cdleme18c  40294  cdleme18d  40296  cdleme19b  40305  cdleme19d  40307  cdleme19e  40308  cdleme20c  40312  cdleme20d  40313  cdleme20e  40314  cdleme20f  40315  cdleme20g  40316  cdleme20h  40317  cdleme20j  40319  cdleme20l2  40322  cdleme20l  40323  cdleme20m  40324  cdleme20  40325  cdleme21ct  40330  cdleme21e  40332  cdleme21i  40336  cdleme22aa  40340  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme22f  40347  cdleme26e  40360  cdleme27a  40368  cdleme32e  40446  cdlemg2fv2  40601  cdlemg4a  40609  cdlemg4d  40614  cdlemg4  40618  cdlemg6c  40621  cdlemg8b  40629  cdlemg8c  40630  cdlemg9a  40633  cdlemg9  40635  cdlemg12a  40644  cdlemg12c  40646  cdlemg17dALTN  40665  cdlemg17h  40669  cdlemg18b  40680  cdlemg18c  40681  cdlemg18d  40682  cdlemg18  40683  cdlemg19a  40684  cdlemg21  40687  cdlemg28a  40694  cdlemg31b0a  40696  cdlemg31d  40701  cdlemg33b0  40702  cdlemg33a  40707  cdlemh  40818  cdlemk5  40837  cdlemk6  40838  cdlemk7  40849  cdlemk11  40850  cdlemk12  40851  cdlemk21N  40874  cdlemk20  40875  cdlemk28-3  40909  cdlemk34  40911  cdlemkfid3N  40926  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk55u1  40966  cdlemn2  41196  cdlemn10  41207  dihjustlem  41217