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  40343  cdlema1N  40606  cdlemednpq  41114  cdleme19e  41122  cdleme20h  41131  cdleme20j  41133  cdleme20l2  41136  cdleme20m  41138  cdleme22a  41155  cdleme22cN  41157  cdleme22f2  41162  cdleme26f2ALTN  41179  cdleme37m  41277  cdlemg12f  41463  cdlemg12g  41464  cdlemg12  41465  cdlemg28a  41508  cdlemg29  41520  cdlemg33a  41521  cdlemg36  41529  cdlemk16a  41671  cdlemk21-2N  41706  cdlemk54  41773  dihord10  42038