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  14294  segconeu  36524  4atlem10  40421  lplncvrlvol2  40430  4atex  40891  4atex2-0cOLDN  40895  cdlemd2  41014  cdlemd3  41015  cdlemd4  41016  cdleme0e  41032  cdleme0moN  41040  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme9  41068  cdleme11c  41076  cdleme11dN  41077  cdleme11e  41078  cdleme11fN  41079  cdleme11h  41081  cdleme11j  41082  cdleme11k  41083  cdleme11  41085  cdleme12  41086  cdleme13  41087  cdleme14  41088  cdleme15a  41089  cdleme15b  41090  cdleme15c  41091  cdleme15d  41092  cdleme15  41093  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme16e  41097  cdleme16f  41098  cdleme17d1  41104  cdleme18a  41106  cdleme18b  41107  cdleme18c  41108  cdleme18d  41110  cdleme19b  41119  cdleme19d  41121  cdleme19e  41122  cdleme20c  41126  cdleme20d  41127  cdleme20e  41128  cdleme20f  41129  cdleme20g  41130  cdleme20h  41131  cdleme20j  41133  cdleme20l2  41136  cdleme20l  41137  cdleme20m  41138  cdleme20  41139  cdleme21ct  41144  cdleme21e  41146  cdleme21i  41150  cdleme22aa  41154  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22eALTN  41160  cdleme22f  41161  cdleme26e  41174  cdleme27a  41182  cdleme32e  41260  cdlemg2fv2  41415  cdlemg4a  41423  cdlemg4d  41428  cdlemg4  41432  cdlemg6c  41435  cdlemg8b  41443  cdlemg8c  41444  cdlemg9a  41447  cdlemg9  41449  cdlemg12a  41458  cdlemg12c  41460  cdlemg17dALTN  41479  cdlemg17h  41483  cdlemg18b  41494  cdlemg18c  41495  cdlemg18d  41496  cdlemg18  41497  cdlemg19a  41498  cdlemg21  41501  cdlemg28a  41508  cdlemg31b0a  41510  cdlemg31d  41515  cdlemg33b0  41516  cdlemg33a  41521  cdlemh  41632  cdlemk5  41651  cdlemk6  41652  cdlemk7  41663  cdlemk11  41664  cdlemk12  41665  cdlemk21N  41688  cdlemk20  41689  cdlemk28-3  41723  cdlemk34  41725  cdlemkfid3N  41740  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk55u1  41780  cdlemn2  42010  cdlemn10  42021  dihjustlem  42031