Theorem simp31r 1304

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ps-2c  40027  cdlema1N  40290  cdlemednpq  40798  cdleme19e  40806  cdleme20h  40815  cdleme20j  40817  cdleme20l2  40820  cdleme20m  40822  cdleme22a  40839  cdleme22cN  40841  cdleme22f2  40846  cdleme26f2ALTN  40863  cdleme37m  40961  cdlemg12f  41147  cdlemg12g  41148  cdlemg12  41149  cdlemg28a  41192  cdlemg29  41204  cdlemg33a  41205  cdlemg36  41213  cdlemk16a  41355  cdlemk21-2N  41390  cdlemk54  41457  dihord10  41722