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  14147  segconeu  36076  4atlem10  39726  lplncvrlvol2  39735  4atex  40196  4atex2-0cOLDN  40200  cdlemd2  40319  cdlemd3  40320  cdlemd4  40321  cdleme0e  40337  cdleme0moN  40345  cdleme3g  40354  cdleme3h  40355  cdleme3  40357  cdleme9  40373  cdleme11c  40381  cdleme11dN  40382  cdleme11e  40383  cdleme11fN  40384  cdleme11h  40386  cdleme11j  40387  cdleme11k  40388  cdleme11  40390  cdleme12  40391  cdleme13  40392  cdleme14  40393  cdleme15a  40394  cdleme15b  40395  cdleme15c  40396  cdleme15d  40397  cdleme15  40398  cdleme16b  40399  cdleme16c  40400  cdleme16d  40401  cdleme16e  40402  cdleme16f  40403  cdleme17d1  40409  cdleme18a  40411  cdleme18b  40412  cdleme18c  40413  cdleme18d  40415  cdleme19b  40424  cdleme19d  40426  cdleme19e  40427  cdleme20c  40431  cdleme20d  40432  cdleme20e  40433  cdleme20f  40434  cdleme20g  40435  cdleme20h  40436  cdleme20j  40438  cdleme20l2  40441  cdleme20l  40442  cdleme20m  40443  cdleme20  40444  cdleme21ct  40449  cdleme21e  40451  cdleme21i  40455  cdleme22aa  40459  cdleme22cN  40462  cdleme22d  40463  cdleme22e  40464  cdleme22eALTN  40465  cdleme22f  40466  cdleme26e  40479  cdleme27a  40487  cdleme32e  40565  cdlemg2fv2  40720  cdlemg4a  40728  cdlemg4d  40733  cdlemg4  40737  cdlemg6c  40740  cdlemg8b  40748  cdlemg8c  40749  cdlemg9a  40752  cdlemg9  40754  cdlemg12a  40763  cdlemg12c  40765  cdlemg17dALTN  40784  cdlemg17h  40788  cdlemg18b  40799  cdlemg18c  40800  cdlemg18d  40801  cdlemg18  40802  cdlemg19a  40803  cdlemg21  40806  cdlemg28a  40813  cdlemg31b0a  40815  cdlemg31d  40820  cdlemg33b0  40821  cdlemg33a  40826  cdlemh  40937  cdlemk5  40956  cdlemk6  40957  cdlemk7  40968  cdlemk11  40969  cdlemk12  40970  cdlemk21N  40993  cdlemk20  40994  cdlemk28-3  41028  cdlemk34  41030  cdlemkfid3N  41045  cdlemk35s-id  41058  cdlemk39s-id  41060  cdlemk55u1  41085  cdlemn2  41315  cdlemn10  41326  dihjustlem  41336