Theorem simp31r 1314

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

Assertion

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

Proof of Theorem simp31r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ps-2c  40159  cdlema1N  40422  cdlemednpq  40930  cdleme19e  40938  cdleme20h  40947  cdleme20j  40949  cdleme20l2  40952  cdleme20m  40954  cdleme22a  40971  cdleme22cN  40973  cdleme22f2  40978  cdleme26f2ALTN  40995  cdleme37m  41093  cdlemg12f  41279  cdlemg12g  41280  cdlemg12  41281  cdlemg28a  41324  cdlemg29  41336  cdlemg33a  41337  cdlemg36  41345  cdlemk16a  41487  cdlemk21-2N  41522  cdlemk54  41589  dihord10  41854