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  14173  segconeu  36224  4atlem10  39976  lplncvrlvol2  39985  4atex  40446  4atex2-0cOLDN  40450  cdlemd2  40569  cdlemd3  40570  cdlemd4  40571  cdleme0e  40587  cdleme0moN  40595  cdleme3g  40604  cdleme3h  40605  cdleme3  40607  cdleme9  40623  cdleme11c  40631  cdleme11dN  40632  cdleme11e  40633  cdleme11fN  40634  cdleme11h  40636  cdleme11j  40637  cdleme11k  40638  cdleme11  40640  cdleme12  40641  cdleme13  40642  cdleme14  40643  cdleme15a  40644  cdleme15b  40645  cdleme15c  40646  cdleme15d  40647  cdleme15  40648  cdleme16b  40649  cdleme16c  40650  cdleme16d  40651  cdleme16e  40652  cdleme16f  40653  cdleme17d1  40659  cdleme18a  40661  cdleme18b  40662  cdleme18c  40663  cdleme18d  40665  cdleme19b  40674  cdleme19d  40676  cdleme19e  40677  cdleme20c  40681  cdleme20d  40682  cdleme20e  40683  cdleme20f  40684  cdleme20g  40685  cdleme20h  40686  cdleme20j  40688  cdleme20l2  40691  cdleme20l  40692  cdleme20m  40693  cdleme20  40694  cdleme21ct  40699  cdleme21e  40701  cdleme21i  40705  cdleme22aa  40709  cdleme22cN  40712  cdleme22d  40713  cdleme22e  40714  cdleme22eALTN  40715  cdleme22f  40716  cdleme26e  40729  cdleme27a  40737  cdleme32e  40815  cdlemg2fv2  40970  cdlemg4a  40978  cdlemg4d  40983  cdlemg4  40987  cdlemg6c  40990  cdlemg8b  40998  cdlemg8c  40999  cdlemg9a  41002  cdlemg9  41004  cdlemg12a  41013  cdlemg12c  41015  cdlemg17dALTN  41034  cdlemg17h  41038  cdlemg18b  41049  cdlemg18c  41050  cdlemg18d  41051  cdlemg18  41052  cdlemg19a  41053  cdlemg21  41056  cdlemg28a  41063  cdlemg31b0a  41065  cdlemg31d  41070  cdlemg33b0  41071  cdlemg33a  41076  cdlemh  41187  cdlemk5  41206  cdlemk6  41207  cdlemk7  41218  cdlemk11  41219  cdlemk12  41220  cdlemk21N  41243  cdlemk20  41244  cdlemk28-3  41278  cdlemk34  41280  cdlemkfid3N  41295  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk55u1  41335  cdlemn2  41565  cdlemn10  41576  dihjustlem  41586