Theorem simp21r 1310

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp21r	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓)

Proof of Theorem simp21r

Step	Hyp	Ref	Expression
1		simp1r 1217	. 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  cdleme0moN  41040  cdleme16e  41097  cdleme17d1  41104  cdleme18d  41110  cdleme19d  41121  cdleme20f  41129  cdleme20g  41130  cdleme21ct  41144  cdleme22aa  41154  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22eALTN  41160  cdleme26e  41174  cdleme32e  41260  cdleme32f  41261  cdlemg4  41432  cdlemg18d  41496  cdlemg18  41497  cdlemg19a  41498  cdlemg19  41499  cdlemg21  41501  cdlemg33b0  41516  cdlemk5  41651  cdlemk6  41652  cdlemk7  41663  cdlemk11  41664  cdlemk12  41665  cdlemk21N  41688  cdlemk20  41689  cdlemk28-3  41723  cdlemk34  41725  cdlemkfid3N  41740  cdlemk55u1  41780