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  39901  cdlema1N  40164  cdlemednpq  40672  cdleme19e  40680  cdleme20h  40689  cdleme20j  40691  cdleme20l2  40694  cdleme20m  40696  cdleme22a  40713  cdleme22cN  40715  cdleme22f2  40720  cdleme26f2ALTN  40737  cdleme37m  40835  cdlemg12f  41021  cdlemg12g  41022  cdlemg12  41023  cdlemg28a  41066  cdlemg29  41078  cdlemg33a  41079  cdlemg36  41087  cdlemk16a  41229  cdlemk21-2N  41264  cdlemk54  41331  dihord10  41596