Theorem simp21l 1286

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

Assertion

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

Proof of Theorem simp21l

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  modexp  13600  segconeu  33472  4atlem10  36757  lplncvrlvol2  36766  4atex  37227  4atex2-0cOLDN  37231  cdlemd2  37350  cdlemd3  37351  cdlemd4  37352  cdleme0e  37368  cdleme0moN  37376  cdleme3g  37385  cdleme3h  37386  cdleme3  37388  cdleme9  37404  cdleme11c  37412  cdleme11dN  37413  cdleme11e  37414  cdleme11fN  37415  cdleme11h  37417  cdleme11j  37418  cdleme11k  37419  cdleme11  37421  cdleme12  37422  cdleme13  37423  cdleme14  37424  cdleme15a  37425  cdleme15b  37426  cdleme15c  37427  cdleme15d  37428  cdleme15  37429  cdleme16b  37430  cdleme16c  37431  cdleme16d  37432  cdleme16e  37433  cdleme16f  37434  cdleme17d1  37440  cdleme18a  37442  cdleme18b  37443  cdleme18c  37444  cdleme18d  37446  cdleme19b  37455  cdleme19d  37457  cdleme19e  37458  cdleme20c  37462  cdleme20d  37463  cdleme20e  37464  cdleme20f  37465  cdleme20g  37466  cdleme20h  37467  cdleme20j  37469  cdleme20l2  37472  cdleme20l  37473  cdleme20m  37474  cdleme20  37475  cdleme21ct  37480  cdleme21e  37482  cdleme21i  37486  cdleme22aa  37490  cdleme22cN  37493  cdleme22d  37494  cdleme22e  37495  cdleme22eALTN  37496  cdleme22f  37497  cdleme26e  37510  cdleme27a  37518  cdleme32e  37596  cdlemg2fv2  37751  cdlemg4a  37759  cdlemg4d  37764  cdlemg4  37768  cdlemg6c  37771  cdlemg8b  37779  cdlemg8c  37780  cdlemg9a  37783  cdlemg9  37785  cdlemg12a  37794  cdlemg12c  37796  cdlemg17dALTN  37815  cdlemg17h  37819  cdlemg18b  37830  cdlemg18c  37831  cdlemg18d  37832  cdlemg18  37833  cdlemg19a  37834  cdlemg21  37837  cdlemg28a  37844  cdlemg31b0a  37846  cdlemg31d  37851  cdlemg33b0  37852  cdlemg33a  37857  cdlemh  37968  cdlemk5  37987  cdlemk6  37988  cdlemk7  37999  cdlemk11  38000  cdlemk12  38001  cdlemk21N  38024  cdlemk20  38025  cdlemk28-3  38059  cdlemk34  38061  cdlemkfid3N  38076  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk55u1  38116  cdlemn2  38346  cdlemn10  38357  dihjustlem  38367