Theorem simp31r 1178

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ps-2c  33832  cdlema1N  34095  cdlemednpq  34604  cdleme19e  34613  cdleme20h  34622  cdleme20j  34624  cdleme20l2  34627  cdleme20m  34629  cdleme22a  34646  cdleme22cN  34648  cdleme22f2  34653  cdleme26f2ALTN  34670  cdleme37m  34768  cdlemg12f  34954  cdlemg12g  34955  cdlemg12  34956  cdlemg28a  34999  cdlemg29  35011  cdlemg33a  35012  cdlemg36  35020  cdlemk16a  35162  cdlemk21-2N  35197  cdlemk54  35264  dihord10  35530