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  40553  cdlema1N  40816  cdlemednpq  41324  cdleme19e  41332  cdleme20h  41341  cdleme20j  41343  cdleme20l2  41346  cdleme20m  41348  cdleme22a  41365  cdleme22cN  41367  cdleme22f2  41372  cdleme26f2ALTN  41389  cdleme37m  41487  cdlemg12f  41673  cdlemg12g  41674  cdlemg12  41675  cdlemg28a  41718  cdlemg29  41730  cdlemg33a  41731  cdlemg36  41739  cdlemk16a  41881  cdlemk21-2N  41916  cdlemk54  41983  dihord10  42248