Theorem simp31r 1310

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ps-2c  40112  cdlema1N  40375  cdlemednpq  40883  cdleme19e  40891  cdleme20h  40900  cdleme20j  40902  cdleme20l2  40905  cdleme20m  40907  cdleme22a  40924  cdleme22cN  40926  cdleme22f2  40931  cdleme26f2ALTN  40948  cdleme37m  41046  cdlemg12f  41232  cdlemg12g  41233  cdlemg12  41234  cdlemg28a  41277  cdlemg29  41289  cdlemg33a  41290  cdlemg36  41298  cdlemk16a  41440  cdlemk21-2N  41475  cdlemk54  41542  dihord10  41807