Theorem simp31r 1316

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

Assertion

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

Proof of Theorem simp31r

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ps-2c  40679  cdlema1N  40942  cdlemednpq  41450  cdleme19e  41458  cdleme20h  41467  cdleme20j  41469  cdleme20l2  41472  cdleme20m  41474  cdleme22a  41491  cdleme22cN  41493  cdleme22f2  41498  cdleme26f2ALTN  41515  cdleme37m  41613  cdlemg12f  41799  cdlemg12g  41800  cdlemg12  41801  cdlemg28a  41844  cdlemg29  41856  cdlemg33a  41857  cdlemg36  41865  cdlemk16a  42007  cdlemk21-2N  42042  cdlemk54  42109  dihord10  42374