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  14362  segconeu  36746  4atlem10  40631  lplncvrlvol2  40640  4atex  41101  4atex2-0cOLDN  41105  cdlemd2  41224  cdlemd3  41225  cdlemd4  41226  cdleme0e  41242  cdleme0moN  41250  cdleme3g  41259  cdleme3h  41260  cdleme3  41262  cdleme9  41278  cdleme11c  41286  cdleme11dN  41287  cdleme11e  41288  cdleme11fN  41289  cdleme11h  41291  cdleme11j  41292  cdleme11k  41293  cdleme11  41295  cdleme12  41296  cdleme13  41297  cdleme14  41298  cdleme15a  41299  cdleme15b  41300  cdleme15c  41301  cdleme15d  41302  cdleme15  41303  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme16e  41307  cdleme16f  41308  cdleme17d1  41314  cdleme18a  41316  cdleme18b  41317  cdleme18c  41318  cdleme18d  41320  cdleme19b  41329  cdleme19d  41331  cdleme19e  41332  cdleme20c  41336  cdleme20d  41337  cdleme20e  41338  cdleme20f  41339  cdleme20g  41340  cdleme20h  41341  cdleme20j  41343  cdleme20l2  41346  cdleme20l  41347  cdleme20m  41348  cdleme20  41349  cdleme21ct  41354  cdleme21e  41356  cdleme21i  41360  cdleme22aa  41364  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22eALTN  41370  cdleme22f  41371  cdleme26e  41384  cdleme27a  41392  cdleme32e  41470  cdlemg2fv2  41625  cdlemg4a  41633  cdlemg4d  41638  cdlemg4  41642  cdlemg6c  41645  cdlemg8b  41653  cdlemg8c  41654  cdlemg9a  41657  cdlemg9  41659  cdlemg12a  41668  cdlemg12c  41670  cdlemg17dALTN  41689  cdlemg17h  41693  cdlemg18b  41704  cdlemg18c  41705  cdlemg18d  41706  cdlemg18  41707  cdlemg19a  41708  cdlemg21  41711  cdlemg28a  41718  cdlemg31b0a  41720  cdlemg31d  41725  cdlemg33b0  41726  cdlemg33a  41731  cdlemh  41842  cdlemk5  41861  cdlemk6  41862  cdlemk7  41873  cdlemk11  41874  cdlemk12  41875  cdlemk21N  41898  cdlemk20  41899  cdlemk28-3  41933  cdlemk34  41935  cdlemkfid3N  41950  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk55u1  41990  cdlemn2  42220  cdlemn10  42231  dihjustlem  42241