Theorem simp31r 1297

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ps-2c  39485  cdlema1N  39748  cdlemednpq  40256  cdleme19e  40264  cdleme20h  40273  cdleme20j  40275  cdleme20l2  40278  cdleme20m  40280  cdleme22a  40297  cdleme22cN  40299  cdleme22f2  40304  cdleme26f2ALTN  40321  cdleme37m  40419  cdlemg12f  40605  cdlemg12g  40606  cdlemg12  40607  cdlemg28a  40650  cdlemg29  40662  cdlemg33a  40663  cdlemg36  40671  cdlemk16a  40813  cdlemk21-2N  40848  cdlemk54  40915  dihord10  41180