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 395   ∧ 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 396  df-3an 1087

This theorem is referenced by:  modexp  13934  segconeu  34292  4atlem10  37599  lplncvrlvol2  37608  4atex  38069  4atex2-0cOLDN  38073  cdleme0moN  38218  cdleme16e  38275  cdleme17d1  38282  cdleme18d  38288  cdleme19d  38299  cdleme20f  38307  cdleme20g  38308  cdleme21ct  38322  cdleme22aa  38332  cdleme22cN  38335  cdleme22d  38336  cdleme22e  38337  cdleme22eALTN  38338  cdleme26e  38352  cdleme32e  38438  cdleme32f  38439  cdlemg4  38610  cdlemg18d  38674  cdlemg18  38675  cdlemg19a  38676  cdlemg19  38677  cdlemg21  38679  cdlemg33b0  38694  cdlemk5  38829  cdlemk6  38830  cdlemk7  38841  cdlemk11  38842  cdlemk12  38843  cdlemk21N  38866  cdlemk20  38867  cdlemk28-3  38901  cdlemk34  38903  cdlemkfid3N  38918  cdlemk55u1  38958