Theorem simp21l 1307

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

Assertion

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

Proof of Theorem simp21l

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  modexp  14265  segconeu  36374  4atlem10  40242  lplncvrlvol2  40251  4atex  40712  4atex2-0cOLDN  40716  cdlemd2  40835  cdlemd3  40836  cdlemd4  40837  cdleme0e  40853  cdleme0moN  40861  cdleme3g  40870  cdleme3h  40871  cdleme3  40873  cdleme9  40889  cdleme11c  40897  cdleme11dN  40898  cdleme11e  40899  cdleme11fN  40900  cdleme11h  40902  cdleme11j  40903  cdleme11k  40904  cdleme11  40906  cdleme12  40907  cdleme13  40908  cdleme14  40909  cdleme15a  40910  cdleme15b  40911  cdleme15c  40912  cdleme15d  40913  cdleme15  40914  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme16e  40918  cdleme16f  40919  cdleme17d1  40925  cdleme18a  40927  cdleme18b  40928  cdleme18c  40929  cdleme18d  40931  cdleme19b  40940  cdleme19d  40942  cdleme19e  40943  cdleme20c  40947  cdleme20d  40948  cdleme20e  40949  cdleme20f  40950  cdleme20g  40951  cdleme20h  40952  cdleme20j  40954  cdleme20l2  40957  cdleme20l  40958  cdleme20m  40959  cdleme20  40960  cdleme21ct  40965  cdleme21e  40967  cdleme21i  40971  cdleme22aa  40975  cdleme22cN  40978  cdleme22d  40979  cdleme22e  40980  cdleme22eALTN  40981  cdleme22f  40982  cdleme26e  40995  cdleme27a  41003  cdleme32e  41081  cdlemg2fv2  41236  cdlemg4a  41244  cdlemg4d  41249  cdlemg4  41253  cdlemg6c  41256  cdlemg8b  41264  cdlemg8c  41265  cdlemg9a  41268  cdlemg9  41270  cdlemg12a  41279  cdlemg12c  41281  cdlemg17dALTN  41300  cdlemg17h  41304  cdlemg18b  41315  cdlemg18c  41316  cdlemg18d  41317  cdlemg18  41318  cdlemg19a  41319  cdlemg21  41322  cdlemg28a  41329  cdlemg31b0a  41331  cdlemg31d  41336  cdlemg33b0  41337  cdlemg33a  41342  cdlemh  41453  cdlemk5  41472  cdlemk6  41473  cdlemk7  41484  cdlemk11  41485  cdlemk12  41486  cdlemk21N  41509  cdlemk20  41510  cdlemk28-3  41544  cdlemk34  41546  cdlemkfid3N  41561  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk55u1  41601  cdlemn2  41831  cdlemn10  41842  dihjustlem  41852