Theorem simp32r 1300

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

Assertion

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

Proof of Theorem simp32r

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

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

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  cdlema1N  39773  paddasslem15  39816  4atex2-0aOLDN  40060  4atex3  40063  cdleme19b  40286  cdleme19d  40288  cdleme19e  40289  cdleme20d  40294  cdleme20f  40296  cdleme20g  40297  cdleme21d  40312  cdleme21e  40313  cdleme22cN  40324  cdleme22e  40326  cdleme22f2  40329  cdleme26e  40341  cdleme28a  40352  cdleme37m  40444  cdlemg28b  40685  cdlemk3  40815  cdlemk12  40832  cdlemk12u  40854  cdlemkoatnle-2N  40857  cdlemk13-2N  40858  cdlemkole-2N  40859  cdlemk14-2N  40860  cdlemk15-2N  40861  cdlemk16-2N  40862  cdlemk17-2N  40863  cdlemk18-2N  40868  cdlemk19-2N  40869  cdlemk7u-2N  40870  cdlemk11u-2N  40871  cdlemk20-2N  40874  cdlemk30  40876  cdlemk23-3  40884  cdlemk24-3  40885