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 1134	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  modexp  14161  segconeu  36205  4atlem10  39862  lplncvrlvol2  39871  4atex  40332  4atex2-0cOLDN  40336  cdlemd2  40455  cdlemd3  40456  cdlemd4  40457  cdleme0e  40473  cdleme0moN  40481  cdleme3g  40490  cdleme3h  40491  cdleme3  40493  cdleme9  40509  cdleme11c  40517  cdleme11dN  40518  cdleme11e  40519  cdleme11fN  40520  cdleme11h  40522  cdleme11j  40523  cdleme11k  40524  cdleme11  40526  cdleme12  40527  cdleme13  40528  cdleme14  40529  cdleme15a  40530  cdleme15b  40531  cdleme15c  40532  cdleme15d  40533  cdleme15  40534  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme16e  40538  cdleme16f  40539  cdleme17d1  40545  cdleme18a  40547  cdleme18b  40548  cdleme18c  40549  cdleme18d  40551  cdleme19b  40560  cdleme19d  40562  cdleme19e  40563  cdleme20c  40567  cdleme20d  40568  cdleme20e  40569  cdleme20f  40570  cdleme20g  40571  cdleme20h  40572  cdleme20j  40574  cdleme20l2  40577  cdleme20l  40578  cdleme20m  40579  cdleme20  40580  cdleme21ct  40585  cdleme21e  40587  cdleme21i  40591  cdleme22aa  40595  cdleme22cN  40598  cdleme22d  40599  cdleme22e  40600  cdleme22eALTN  40601  cdleme22f  40602  cdleme26e  40615  cdleme27a  40623  cdleme32e  40701  cdlemg2fv2  40856  cdlemg4a  40864  cdlemg4d  40869  cdlemg4  40873  cdlemg6c  40876  cdlemg8b  40884  cdlemg8c  40885  cdlemg9a  40888  cdlemg9  40890  cdlemg12a  40899  cdlemg12c  40901  cdlemg17dALTN  40920  cdlemg17h  40924  cdlemg18b  40935  cdlemg18c  40936  cdlemg18d  40937  cdlemg18  40938  cdlemg19a  40939  cdlemg21  40942  cdlemg28a  40949  cdlemg31b0a  40951  cdlemg31d  40956  cdlemg33b0  40957  cdlemg33a  40962  cdlemh  41073  cdlemk5  41092  cdlemk6  41093  cdlemk7  41104  cdlemk11  41105  cdlemk12  41106  cdlemk21N  41129  cdlemk20  41130  cdlemk28-3  41164  cdlemk34  41166  cdlemkfid3N  41181  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk55u1  41221  cdlemn2  41451  cdlemn10  41462  dihjustlem  41472