Theorem simp31r 1316

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

Assertion

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

Proof of Theorem simp31r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ps-2c  40409  cdlema1N  40672  cdlemednpq  41180  cdleme19e  41188  cdleme20h  41197  cdleme20j  41199  cdleme20l2  41202  cdleme20m  41204  cdleme22a  41221  cdleme22cN  41223  cdleme22f2  41228  cdleme26f2ALTN  41245  cdleme37m  41343  cdlemg12f  41529  cdlemg12g  41530  cdlemg12  41531  cdlemg28a  41574  cdlemg29  41586  cdlemg33a  41587  cdlemg36  41595  cdlemk16a  41737  cdlemk21-2N  41772  cdlemk54  41839  dihord10  42104