Theorem simp32r 1298

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

Assertion

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

Proof of Theorem simp32r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  cdlema1N  37805  paddasslem15  37848  4atex2-0aOLDN  38092  4atex3  38095  cdleme19b  38318  cdleme19d  38320  cdleme19e  38321  cdleme20d  38326  cdleme20f  38328  cdleme20g  38329  cdleme21d  38344  cdleme21e  38345  cdleme22cN  38356  cdleme22e  38358  cdleme22f2  38361  cdleme26e  38373  cdleme28a  38384  cdleme37m  38476  cdlemg28b  38717  cdlemk3  38847  cdlemk12  38864  cdlemk12u  38886  cdlemkoatnle-2N  38889  cdlemk13-2N  38890  cdlemkole-2N  38891  cdlemk14-2N  38892  cdlemk15-2N  38893  cdlemk16-2N  38894  cdlemk17-2N  38895  cdlemk18-2N  38900  cdlemk19-2N  38901  cdlemk7u-2N  38902  cdlemk11u-2N  38903  cdlemk20-2N  38906  cdlemk30  38908  cdlemk23-3  38916  cdlemk24-3  38917