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  39988  cdlema1N  40251  cdlemednpq  40759  cdleme19e  40767  cdleme20h  40776  cdleme20j  40778  cdleme20l2  40781  cdleme20m  40783  cdleme22a  40800  cdleme22cN  40802  cdleme22f2  40807  cdleme26f2ALTN  40824  cdleme37m  40922  cdlemg12f  41108  cdlemg12g  41109  cdlemg12  41110  cdlemg28a  41153  cdlemg29  41165  cdlemg33a  41166  cdlemg36  41174  cdlemk16a  41316  cdlemk21-2N  41351  cdlemk54  41418  dihord10  41683