Theorem simp21r 1289

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

Assertion

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

Proof of Theorem simp21r

Step	Hyp	Ref	Expression
1		simp1r 1196	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant2 1132	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087

This theorem is referenced by:  modexp  14205  segconeu  35287  4atlem10  38780  lplncvrlvol2  38789  4atex  39250  4atex2-0cOLDN  39254  cdleme0moN  39399  cdleme16e  39456  cdleme17d1  39463  cdleme18d  39469  cdleme19d  39480  cdleme20f  39488  cdleme20g  39489  cdleme21ct  39503  cdleme22aa  39513  cdleme22cN  39516  cdleme22d  39517  cdleme22e  39518  cdleme22eALTN  39519  cdleme26e  39533  cdleme32e  39619  cdleme32f  39620  cdlemg4  39791  cdlemg18d  39855  cdlemg18  39856  cdlemg19a  39857  cdlemg19  39858  cdlemg21  39860  cdlemg33b0  39875  cdlemk5  40010  cdlemk6  40011  cdlemk7  40022  cdlemk11  40023  cdlemk12  40024  cdlemk21N  40047  cdlemk20  40048  cdlemk28-3  40082  cdlemk34  40084  cdlemkfid3N  40099  cdlemk55u1  40139