Theorem simp31r 1382

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

Assertion

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

Proof of Theorem simp31r

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

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

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  ps-2c  35317  cdlema1N  35580  cdlemednpq  36089  cdleme19e  36097  cdleme20h  36106  cdleme20j  36108  cdleme20l2  36111  cdleme20m  36113  cdleme22a  36130  cdleme22cN  36132  cdleme22f2  36137  cdleme26f2ALTN  36154  cdleme37m  36252  cdlemg12f  36438  cdlemg12g  36439  cdlemg12  36440  cdlemg28a  36483  cdlemg29  36495  cdlemg33a  36496  cdlemg36  36504  cdlemk16a  36646  cdlemk21-2N  36681  cdlemk54  36748  dihord10  37014