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 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  14277  segconeu  36012  4atlem10  39608  lplncvrlvol2  39617  4atex  40078  4atex2-0cOLDN  40082  cdlemd2  40201  cdlemd3  40202  cdlemd4  40203  cdleme0e  40219  cdleme0moN  40227  cdleme3g  40236  cdleme3h  40237  cdleme3  40239  cdleme9  40255  cdleme11c  40263  cdleme11dN  40264  cdleme11e  40265  cdleme11fN  40266  cdleme11h  40268  cdleme11j  40269  cdleme11k  40270  cdleme11  40272  cdleme12  40273  cdleme13  40274  cdleme14  40275  cdleme15a  40276  cdleme15b  40277  cdleme15c  40278  cdleme15d  40279  cdleme15  40280  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme16f  40285  cdleme17d1  40291  cdleme18a  40293  cdleme18b  40294  cdleme18c  40295  cdleme18d  40297  cdleme19b  40306  cdleme19d  40308  cdleme19e  40309  cdleme20c  40313  cdleme20d  40314  cdleme20e  40315  cdleme20f  40316  cdleme20g  40317  cdleme20h  40318  cdleme20j  40320  cdleme20l2  40323  cdleme20l  40324  cdleme20m  40325  cdleme20  40326  cdleme21ct  40331  cdleme21e  40333  cdleme21i  40337  cdleme22aa  40341  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme22f  40348  cdleme26e  40361  cdleme27a  40369  cdleme32e  40447  cdlemg2fv2  40602  cdlemg4a  40610  cdlemg4d  40615  cdlemg4  40619  cdlemg6c  40622  cdlemg8b  40630  cdlemg8c  40631  cdlemg9a  40634  cdlemg9  40636  cdlemg12a  40645  cdlemg12c  40647  cdlemg17dALTN  40666  cdlemg17h  40670  cdlemg18b  40681  cdlemg18c  40682  cdlemg18d  40683  cdlemg18  40684  cdlemg19a  40685  cdlemg21  40688  cdlemg28a  40695  cdlemg31b0a  40697  cdlemg31d  40702  cdlemg33b0  40703  cdlemg33a  40708  cdlemh  40819  cdlemk5  40838  cdlemk6  40839  cdlemk7  40850  cdlemk11  40851  cdlemk12  40852  cdlemk21N  40875  cdlemk20  40876  cdlemk28-3  40910  cdlemk34  40912  cdlemkfid3N  40927  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk55u1  40967  cdlemn2  41197  cdlemn10  41208  dihjustlem  41218