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 ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ps-2c  40283  cdlema1N  40546  cdlemednpq  41054  cdleme19e  41062  cdleme20h  41071  cdleme20j  41073  cdleme20l2  41076  cdleme20m  41078  cdleme22a  41095  cdleme22cN  41097  cdleme22f2  41102  cdleme26f2ALTN  41119  cdleme37m  41217  cdlemg12f  41403  cdlemg12g  41404  cdlemg12  41405  cdlemg28a  41448  cdlemg29  41460  cdlemg33a  41461  cdlemg36  41469  cdlemk16a  41611  cdlemk21-2N  41646  cdlemk54  41713  dihord10  41978