Theorem simp21l 1178

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

Assertion

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

Proof of Theorem simp21l

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  modexp  12999  segconeu  32118  4atlem10  34892  lplncvrlvol2  34901  4atex  35362  4atex2-0cOLDN  35366  cdlemd2  35486  cdlemd3  35487  cdlemd4  35488  cdleme0e  35504  cdleme0moN  35512  cdleme3g  35521  cdleme3h  35522  cdleme3  35524  cdleme9  35540  cdleme11c  35548  cdleme11dN  35549  cdleme11e  35550  cdleme11fN  35551  cdleme11h  35553  cdleme11j  35554  cdleme11k  35555  cdleme11  35557  cdleme12  35558  cdleme13  35559  cdleme14  35560  cdleme15a  35561  cdleme15b  35562  cdleme15c  35563  cdleme15d  35564  cdleme15  35565  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme17d1  35576  cdleme18a  35578  cdleme18b  35579  cdleme18c  35580  cdleme18d  35582  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20c  35599  cdleme20d  35600  cdleme20e  35601  cdleme20f  35602  cdleme20g  35603  cdleme20h  35604  cdleme20j  35606  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme20  35612  cdleme21ct  35617  cdleme21e  35619  cdleme21i  35623  cdleme22aa  35627  cdleme22cN  35630  cdleme22d  35631  cdleme22e  35632  cdleme22eALTN  35633  cdleme22f  35634  cdleme26e  35647  cdleme27a  35655  cdleme32e  35733  cdlemg2fv2  35888  cdlemg4a  35896  cdlemg4d  35901  cdlemg4  35905  cdlemg6c  35908  cdlemg8b  35916  cdlemg8c  35917  cdlemg9a  35920  cdlemg9  35922  cdlemg12a  35931  cdlemg12c  35933  cdlemg17dALTN  35952  cdlemg17h  35956  cdlemg18b  35967  cdlemg18c  35968  cdlemg18d  35969  cdlemg18  35970  cdlemg19a  35971  cdlemg21  35974  cdlemg28a  35981  cdlemg31b0a  35983  cdlemg31d  35988  cdlemg33b0  35989  cdlemg33a  35994  cdlemh  36105  cdlemk5  36124  cdlemk6  36125  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemk21N  36161  cdlemk20  36162  cdlemk28-3  36196  cdlemk34  36198  cdlemkfid3N  36213  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk55u1  36253  cdlemn2  36484  cdlemn10  36495  dihjustlem  36505