Theorem simp21l 1309

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

Assertion

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

Proof of Theorem simp21l

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  modexp  14386  segconeu  36869  4atlem10  40757  lplncvrlvol2  40766  4atex  41227  4atex2-0cOLDN  41231  cdlemd2  41350  cdlemd3  41351  cdlemd4  41352  cdleme0e  41368  cdleme0moN  41376  cdleme3g  41385  cdleme3h  41386  cdleme3  41388  cdleme9  41404  cdleme11c  41412  cdleme11dN  41413  cdleme11e  41414  cdleme11fN  41415  cdleme11h  41417  cdleme11j  41418  cdleme11k  41419  cdleme11  41421  cdleme12  41422  cdleme13  41423  cdleme14  41424  cdleme15a  41425  cdleme15b  41426  cdleme15c  41427  cdleme15d  41428  cdleme15  41429  cdleme16b  41430  cdleme16c  41431  cdleme16d  41432  cdleme16e  41433  cdleme16f  41434  cdleme17d1  41440  cdleme18a  41442  cdleme18b  41443  cdleme18c  41444  cdleme18d  41446  cdleme19b  41455  cdleme19d  41457  cdleme19e  41458  cdleme20c  41462  cdleme20d  41463  cdleme20e  41464  cdleme20f  41465  cdleme20g  41466  cdleme20h  41467  cdleme20j  41469  cdleme20l2  41472  cdleme20l  41473  cdleme20m  41474  cdleme20  41475  cdleme21ct  41480  cdleme21e  41482  cdleme21i  41486  cdleme22aa  41490  cdleme22cN  41493  cdleme22d  41494  cdleme22e  41495  cdleme22eALTN  41496  cdleme22f  41497  cdleme26e  41510  cdleme27a  41518  cdleme32e  41596  cdlemg2fv2  41751  cdlemg4a  41759  cdlemg4d  41764  cdlemg4  41768  cdlemg6c  41771  cdlemg8b  41779  cdlemg8c  41780  cdlemg9a  41783  cdlemg9  41785  cdlemg12a  41794  cdlemg12c  41796  cdlemg17dALTN  41815  cdlemg17h  41819  cdlemg18b  41830  cdlemg18c  41831  cdlemg18d  41832  cdlemg18  41833  cdlemg19a  41834  cdlemg21  41837  cdlemg28a  41844  cdlemg31b0a  41846  cdlemg31d  41851  cdlemg33b0  41852  cdlemg33a  41857  cdlemh  41968  cdlemk5  41987  cdlemk6  41988  cdlemk7  41999  cdlemk11  42000  cdlemk12  42001  cdlemk21N  42024  cdlemk20  42025  cdlemk28-3  42059  cdlemk34  42061  cdlemkfid3N  42076  cdlemk35s-id  42089  cdlemk39s-id  42091  cdlemk55u1  42116  cdlemn2  42346  cdlemn10  42357  dihjustlem  42367