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  14409  segconeu  36954  4atlem10  40855  lplncvrlvol2  40864  4atex  41325  4atex2-0cOLDN  41329  cdleme0moN  41474  cdleme16e  41531  cdleme17d1  41538  cdleme18d  41544  cdleme19d  41555  cdleme20f  41563  cdleme20g  41564  cdleme21ct  41578  cdleme22aa  41588  cdleme22cN  41591  cdleme22d  41592  cdleme22e  41593  cdleme22eALTN  41594  cdleme26e  41608  cdleme32e  41694  cdleme32f  41695  cdlemg4  41866  cdlemg18d  41930  cdlemg18  41931  cdlemg19a  41932  cdlemg19  41933  cdlemg21  41935  cdlemg33b0  41950  cdlemk5  42085  cdlemk6  42086  cdlemk7  42097  cdlemk11  42098  cdlemk12  42099  cdlemk21N  42122  cdlemk20  42123  cdlemk28-3  42157  cdlemk34  42159  cdlemkfid3N  42174  cdlemk55u1  42214