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  14412  segconeu  36967  4atlem10  40866  lplncvrlvol2  40875  4atex  41336  4atex2-0cOLDN  41340  cdlemd2  41459  cdlemd3  41460  cdlemd4  41461  cdleme0e  41477  cdleme0moN  41485  cdleme3g  41494  cdleme3h  41495  cdleme3  41497  cdleme9  41513  cdleme11c  41521  cdleme11dN  41522  cdleme11e  41523  cdleme11fN  41524  cdleme11h  41526  cdleme11j  41527  cdleme11k  41528  cdleme11  41530  cdleme12  41531  cdleme13  41532  cdleme14  41533  cdleme15a  41534  cdleme15b  41535  cdleme15c  41536  cdleme15d  41537  cdleme15  41538  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme16e  41542  cdleme16f  41543  cdleme17d1  41549  cdleme18a  41551  cdleme18b  41552  cdleme18c  41553  cdleme18d  41555  cdleme19b  41564  cdleme19d  41566  cdleme19e  41567  cdleme20c  41571  cdleme20d  41572  cdleme20e  41573  cdleme20f  41574  cdleme20g  41575  cdleme20h  41576  cdleme20j  41578  cdleme20l2  41581  cdleme20l  41582  cdleme20m  41583  cdleme20  41584  cdleme21ct  41589  cdleme21e  41591  cdleme21i  41595  cdleme22aa  41599  cdleme22cN  41602  cdleme22d  41603  cdleme22e  41604  cdleme22eALTN  41605  cdleme22f  41606  cdleme26e  41619  cdleme27a  41627  cdleme32e  41705  cdlemg2fv2  41860  cdlemg4a  41868  cdlemg4d  41873  cdlemg4  41877  cdlemg6c  41880  cdlemg8b  41888  cdlemg8c  41889  cdlemg9a  41892  cdlemg9  41894  cdlemg12a  41903  cdlemg12c  41905  cdlemg17dALTN  41924  cdlemg17h  41928  cdlemg18b  41939  cdlemg18c  41940  cdlemg18d  41941  cdlemg18  41942  cdlemg19a  41943  cdlemg21  41946  cdlemg28a  41953  cdlemg31b0a  41955  cdlemg31d  41960  cdlemg33b0  41961  cdlemg33a  41966  cdlemh  42077  cdlemk5  42096  cdlemk6  42097  cdlemk7  42108  cdlemk11  42109  cdlemk12  42110  cdlemk21N  42133  cdlemk20  42134  cdlemk28-3  42168  cdlemk34  42170  cdlemkfid3N  42185  cdlemk35s-id  42198  cdlemk39s-id  42200  cdlemk55u1  42225  cdlemn2  42455  cdlemn10  42466  dihjustlem  42476