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  14306  segconeu  36599  4atlem10  40487  lplncvrlvol2  40496  4atex  40957  4atex2-0cOLDN  40961  cdlemd2  41080  cdlemd3  41081  cdlemd4  41082  cdleme0e  41098  cdleme0moN  41106  cdleme3g  41115  cdleme3h  41116  cdleme3  41118  cdleme9  41134  cdleme11c  41142  cdleme11dN  41143  cdleme11e  41144  cdleme11fN  41145  cdleme11h  41147  cdleme11j  41148  cdleme11k  41149  cdleme11  41151  cdleme12  41152  cdleme13  41153  cdleme14  41154  cdleme15a  41155  cdleme15b  41156  cdleme15c  41157  cdleme15d  41158  cdleme15  41159  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme16e  41163  cdleme16f  41164  cdleme17d1  41170  cdleme18a  41172  cdleme18b  41173  cdleme18c  41174  cdleme18d  41176  cdleme19b  41185  cdleme19d  41187  cdleme19e  41188  cdleme20c  41192  cdleme20d  41193  cdleme20e  41194  cdleme20f  41195  cdleme20g  41196  cdleme20h  41197  cdleme20j  41199  cdleme20l2  41202  cdleme20l  41203  cdleme20m  41204  cdleme20  41205  cdleme21ct  41210  cdleme21e  41212  cdleme21i  41216  cdleme22aa  41220  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22eALTN  41226  cdleme22f  41227  cdleme26e  41240  cdleme27a  41248  cdleme32e  41326  cdlemg2fv2  41481  cdlemg4a  41489  cdlemg4d  41494  cdlemg4  41498  cdlemg6c  41501  cdlemg8b  41509  cdlemg8c  41510  cdlemg9a  41513  cdlemg9  41515  cdlemg12a  41524  cdlemg12c  41526  cdlemg17dALTN  41545  cdlemg17h  41549  cdlemg18b  41560  cdlemg18c  41561  cdlemg18d  41562  cdlemg18  41563  cdlemg19a  41564  cdlemg21  41567  cdlemg28a  41574  cdlemg31b0a  41576  cdlemg31d  41581  cdlemg33b0  41582  cdlemg33a  41587  cdlemh  41698  cdlemk5  41717  cdlemk6  41718  cdlemk7  41729  cdlemk11  41730  cdlemk12  41731  cdlemk21N  41754  cdlemk20  41755  cdlemk28-3  41789  cdlemk34  41791  cdlemkfid3N  41806  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk55u1  41846  cdlemn2  42076  cdlemn10  42087  dihjustlem  42097