Theorem simp32r 1296

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

Assertion

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

Proof of Theorem simp32r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  cdlema1N  37402  paddasslem15  37445  4atex2-0aOLDN  37689  4atex3  37692  cdleme19b  37915  cdleme19d  37917  cdleme19e  37918  cdleme20d  37923  cdleme20f  37925  cdleme20g  37926  cdleme21d  37941  cdleme21e  37942  cdleme22cN  37953  cdleme22e  37955  cdleme22f2  37958  cdleme26e  37970  cdleme28a  37981  cdleme37m  38073  cdlemg28b  38314  cdlemk3  38444  cdlemk12  38461  cdlemk12u  38483  cdlemkoatnle-2N  38486  cdlemk13-2N  38487  cdlemkole-2N  38488  cdlemk14-2N  38489  cdlemk15-2N  38490  cdlemk16-2N  38491  cdlemk17-2N  38492  cdlemk18-2N  38497  cdlemk19-2N  38498  cdlemk7u-2N  38499  cdlemk11u-2N  38500  cdlemk20-2N  38503  cdlemk30  38505  cdlemk23-3  38513  cdlemk24-3  38514