Theorem simp32r 1297

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

Assertion

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

Proof of Theorem simp32r

Step	Hyp	Ref	Expression
1		simp2r 1198	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant3 1133	1 ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  cdlema1N  39201  paddasslem15  39244  4atex2-0aOLDN  39488  4atex3  39491  cdleme19b  39714  cdleme19d  39716  cdleme19e  39717  cdleme20d  39722  cdleme20f  39724  cdleme20g  39725  cdleme21d  39740  cdleme21e  39741  cdleme22cN  39752  cdleme22e  39754  cdleme22f2  39757  cdleme26e  39769  cdleme28a  39780  cdleme37m  39872  cdlemg28b  40113  cdlemk3  40243  cdlemk12  40260  cdlemk12u  40282  cdlemkoatnle-2N  40285  cdlemk13-2N  40286  cdlemkole-2N  40287  cdlemk14-2N  40288  cdlemk15-2N  40289  cdlemk16-2N  40290  cdlemk17-2N  40291  cdlemk18-2N  40296  cdlemk19-2N  40297  cdlemk7u-2N  40298  cdlemk11u-2N  40299  cdlemk20-2N  40302  cdlemk30  40304  cdlemk23-3  40312  cdlemk24-3  40313