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  14306  segconeu  36599  4atlem10  40487  lplncvrlvol2  40496  4atex  40957  4atex2-0cOLDN  40961  cdleme0moN  41106  cdleme16e  41163  cdleme17d1  41170  cdleme18d  41176  cdleme19d  41187  cdleme20f  41195  cdleme20g  41196  cdleme21ct  41210  cdleme22aa  41220  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22eALTN  41226  cdleme26e  41240  cdleme32e  41326  cdleme32f  41327  cdlemg4  41498  cdlemg18d  41562  cdlemg18  41563  cdlemg19a  41564  cdlemg19  41565  cdlemg21  41567  cdlemg33b0  41582  cdlemk5  41717  cdlemk6  41718  cdlemk7  41729  cdlemk11  41730  cdlemk12  41731  cdlemk21N  41754  cdlemk20  41755  cdlemk28-3  41789  cdlemk34  41791  cdlemkfid3N  41806  cdlemk55u1  41846