Theorem simp21r 1290

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

Assertion

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

Proof of Theorem simp21r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  modexp  13941  segconeu  34299  4atlem10  37606  lplncvrlvol2  37615  4atex  38076  4atex2-0cOLDN  38080  cdleme0moN  38225  cdleme16e  38282  cdleme17d1  38289  cdleme18d  38295  cdleme19d  38306  cdleme20f  38314  cdleme20g  38315  cdleme21ct  38329  cdleme22aa  38339  cdleme22cN  38342  cdleme22d  38343  cdleme22e  38344  cdleme22eALTN  38345  cdleme26e  38359  cdleme32e  38445  cdleme32f  38446  cdlemg4  38617  cdlemg18d  38681  cdlemg18  38682  cdlemg19a  38683  cdlemg19  38684  cdlemg21  38686  cdlemg33b0  38701  cdlemk5  38836  cdlemk6  38837  cdlemk7  38848  cdlemk11  38849  cdlemk12  38850  cdlemk21N  38873  cdlemk20  38874  cdlemk28-3  38908  cdlemk34  38910  cdlemkfid3N  38925  cdlemk55u1  38965