Theorem simp21l 1303

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

Assertion

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

Proof of Theorem simp21l

Step	Hyp	Ref	Expression
1		simp1l 1210	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	3ad2ant2 1146	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  modexp  14248  segconeu  36325  4atlem10  40194  lplncvrlvol2  40203  4atex  40664  4atex2-0cOLDN  40668  cdlemd2  40787  cdlemd3  40788  cdlemd4  40789  cdleme0e  40805  cdleme0moN  40813  cdleme3g  40822  cdleme3h  40823  cdleme3  40825  cdleme9  40841  cdleme11c  40849  cdleme11dN  40850  cdleme11e  40851  cdleme11fN  40852  cdleme11h  40854  cdleme11j  40855  cdleme11k  40856  cdleme11  40858  cdleme12  40859  cdleme13  40860  cdleme14  40861  cdleme15a  40862  cdleme15b  40863  cdleme15c  40864  cdleme15d  40865  cdleme15  40866  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme16e  40870  cdleme16f  40871  cdleme17d1  40877  cdleme18a  40879  cdleme18b  40880  cdleme18c  40881  cdleme18d  40883  cdleme19b  40892  cdleme19d  40894  cdleme19e  40895  cdleme20c  40899  cdleme20d  40900  cdleme20e  40901  cdleme20f  40902  cdleme20g  40903  cdleme20h  40904  cdleme20j  40906  cdleme20l2  40909  cdleme20l  40910  cdleme20m  40911  cdleme20  40912  cdleme21ct  40917  cdleme21e  40919  cdleme21i  40923  cdleme22aa  40927  cdleme22cN  40930  cdleme22d  40931  cdleme22e  40932  cdleme22eALTN  40933  cdleme22f  40934  cdleme26e  40947  cdleme27a  40955  cdleme32e  41033  cdlemg2fv2  41188  cdlemg4a  41196  cdlemg4d  41201  cdlemg4  41205  cdlemg6c  41208  cdlemg8b  41216  cdlemg8c  41217  cdlemg9a  41220  cdlemg9  41222  cdlemg12a  41231  cdlemg12c  41233  cdlemg17dALTN  41252  cdlemg17h  41256  cdlemg18b  41267  cdlemg18c  41268  cdlemg18d  41269  cdlemg18  41270  cdlemg19a  41271  cdlemg21  41274  cdlemg28a  41281  cdlemg31b0a  41283  cdlemg31d  41288  cdlemg33b0  41289  cdlemg33a  41294  cdlemh  41405  cdlemk5  41424  cdlemk6  41425  cdlemk7  41436  cdlemk11  41437  cdlemk12  41438  cdlemk21N  41461  cdlemk20  41462  cdlemk28-3  41496  cdlemk34  41498  cdlemkfid3N  41513  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk55u1  41553  cdlemn2  41783  cdlemn10  41794  dihjustlem  41804