Theorem simp31r 1380

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

Assertion

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

Proof of Theorem simp31r

Step	Hyp	Ref	Expression
1		simp1r 1239	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓)
2	1	3ad2ant3 1128	1 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1070

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 197  df-an 383  df-3an 1072

This theorem is referenced by:  ps-2c  35329  cdlema1N  35592  cdlemednpq  36101  cdleme19e  36109  cdleme20h  36118  cdleme20j  36120  cdleme20l2  36123  cdleme20m  36125  cdleme22a  36142  cdleme22cN  36144  cdleme22f2  36149  cdleme26f2ALTN  36166  cdleme37m  36264  cdlemg12f  36450  cdlemg12g  36451  cdlemg12  36452  cdlemg28a  36495  cdlemg29  36507  cdlemg33a  36508  cdlemg36  36516  cdlemk16a  36658  cdlemk21-2N  36693  cdlemk54  36760  dihord10  37026