Theorem simp31r 1299

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ps-2c  39974  cdlema1N  40237  cdlemednpq  40745  cdleme19e  40753  cdleme20h  40762  cdleme20j  40764  cdleme20l2  40767  cdleme20m  40769  cdleme22a  40786  cdleme22cN  40788  cdleme22f2  40793  cdleme26f2ALTN  40810  cdleme37m  40908  cdlemg12f  41094  cdlemg12g  41095  cdlemg12  41096  cdlemg28a  41139  cdlemg29  41151  cdlemg33a  41152  cdlemg36  41160  cdlemk16a  41302  cdlemk21-2N  41337  cdlemk54  41404  dihord10  41669