Theorem simp32r 1316

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

Assertion

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

Proof of Theorem simp32r

Step	Hyp	Ref	Expression
1		simp2r 1217	. 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:  cdlema1N  40422  paddasslem15  40465  4atex2-0aOLDN  40709  4atex3  40712  cdleme19b  40935  cdleme19d  40937  cdleme19e  40938  cdleme20d  40943  cdleme20f  40945  cdleme20g  40946  cdleme21d  40961  cdleme21e  40962  cdleme22cN  40973  cdleme22e  40975  cdleme22f2  40978  cdleme26e  40990  cdleme28a  41001  cdleme37m  41093  cdlemg28b  41334  cdlemk3  41464  cdlemk12  41481  cdlemk12u  41503  cdlemkoatnle-2N  41506  cdlemk13-2N  41507  cdlemkole-2N  41508  cdlemk14-2N  41509  cdlemk15-2N  41510  cdlemk16-2N  41511  cdlemk17-2N  41512  cdlemk18-2N  41517  cdlemk19-2N  41518  cdlemk7u-2N  41519  cdlemk11u-2N  41520  cdlemk20-2N  41523  cdlemk30  41525  cdlemk23-3  41533  cdlemk24-3  41534