Theorem simp21l 1292

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1199	. 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  14191  segconeu  36209  4atlem10  40066  lplncvrlvol2  40075  4atex  40536  4atex2-0cOLDN  40540  cdlemd2  40659  cdlemd3  40660  cdlemd4  40661  cdleme0e  40677  cdleme0moN  40685  cdleme3g  40694  cdleme3h  40695  cdleme3  40697  cdleme9  40713  cdleme11c  40721  cdleme11dN  40722  cdleme11e  40723  cdleme11fN  40724  cdleme11h  40726  cdleme11j  40727  cdleme11k  40728  cdleme11  40730  cdleme12  40731  cdleme13  40732  cdleme14  40733  cdleme15a  40734  cdleme15b  40735  cdleme15c  40736  cdleme15d  40737  cdleme15  40738  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme16f  40743  cdleme17d1  40749  cdleme18a  40751  cdleme18b  40752  cdleme18c  40753  cdleme18d  40755  cdleme19b  40764  cdleme19d  40766  cdleme19e  40767  cdleme20c  40771  cdleme20d  40772  cdleme20e  40773  cdleme20f  40774  cdleme20g  40775  cdleme20h  40776  cdleme20j  40778  cdleme20l2  40781  cdleme20l  40782  cdleme20m  40783  cdleme20  40784  cdleme21ct  40789  cdleme21e  40791  cdleme21i  40795  cdleme22aa  40799  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme22f  40806  cdleme26e  40819  cdleme27a  40827  cdleme32e  40905  cdlemg2fv2  41060  cdlemg4a  41068  cdlemg4d  41073  cdlemg4  41077  cdlemg6c  41080  cdlemg8b  41088  cdlemg8c  41089  cdlemg9a  41092  cdlemg9  41094  cdlemg12a  41103  cdlemg12c  41105  cdlemg17dALTN  41124  cdlemg17h  41128  cdlemg18b  41139  cdlemg18c  41140  cdlemg18d  41141  cdlemg18  41142  cdlemg19a  41143  cdlemg21  41146  cdlemg28a  41153  cdlemg31b0a  41155  cdlemg31d  41160  cdlemg33b0  41161  cdlemg33a  41166  cdlemh  41277  cdlemk5  41296  cdlemk6  41297  cdlemk7  41308  cdlemk11  41309  cdlemk12  41310  cdlemk21N  41333  cdlemk20  41334  cdlemk28-3  41368  cdlemk34  41370  cdlemkfid3N  41385  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk55u1  41425  cdlemn2  41655  cdlemn10  41666  dihjustlem  41676