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  14200  segconeu  36193  4atlem10  40052  lplncvrlvol2  40061  4atex  40522  4atex2-0cOLDN  40526  cdlemd2  40645  cdlemd3  40646  cdlemd4  40647  cdleme0e  40663  cdleme0moN  40671  cdleme3g  40680  cdleme3h  40681  cdleme3  40683  cdleme9  40699  cdleme11c  40707  cdleme11dN  40708  cdleme11e  40709  cdleme11fN  40710  cdleme11h  40712  cdleme11j  40713  cdleme11k  40714  cdleme11  40716  cdleme12  40717  cdleme13  40718  cdleme14  40719  cdleme15a  40720  cdleme15b  40721  cdleme15c  40722  cdleme15d  40723  cdleme15  40724  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme16f  40729  cdleme17d1  40735  cdleme18a  40737  cdleme18b  40738  cdleme18c  40739  cdleme18d  40741  cdleme19b  40750  cdleme19d  40752  cdleme19e  40753  cdleme20c  40757  cdleme20d  40758  cdleme20e  40759  cdleme20f  40760  cdleme20g  40761  cdleme20h  40762  cdleme20j  40764  cdleme20l2  40767  cdleme20l  40768  cdleme20m  40769  cdleme20  40770  cdleme21ct  40775  cdleme21e  40777  cdleme21i  40781  cdleme22aa  40785  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme22f  40792  cdleme26e  40805  cdleme27a  40813  cdleme32e  40891  cdlemg2fv2  41046  cdlemg4a  41054  cdlemg4d  41059  cdlemg4  41063  cdlemg6c  41066  cdlemg8b  41074  cdlemg8c  41075  cdlemg9a  41078  cdlemg9  41080  cdlemg12a  41089  cdlemg12c  41091  cdlemg17dALTN  41110  cdlemg17h  41114  cdlemg18b  41125  cdlemg18c  41126  cdlemg18d  41127  cdlemg18  41128  cdlemg19a  41129  cdlemg21  41132  cdlemg28a  41139  cdlemg31b0a  41141  cdlemg31d  41146  cdlemg33b0  41147  cdlemg33a  41152  cdlemh  41263  cdlemk5  41282  cdlemk6  41283  cdlemk7  41294  cdlemk11  41295  cdlemk12  41296  cdlemk21N  41319  cdlemk20  41320  cdlemk28-3  41354  cdlemk34  41356  cdlemkfid3N  41371  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk55u1  41411  cdlemn2  41641  cdlemn10  41652  dihjustlem  41662