Theorem ecase33d

Description: Deduction for elimination by cases. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	ecase33d.1	$$⊢\phi \to \neg \psi$$
	ecase33d.2	$$⊢\phi \to \neg \chi$$
	ecase33d.3	$$⊢\phi \to \left(\psi \vee \chi \vee \theta \right)$$
Assertion	ecase33d	$$⊢\phi \to \theta$$

Proof

Step	Hyp	Ref	Expression
1		ecase33d.1	$$⊢\phi \to \neg \psi$$
2		ecase33d.2	$$⊢\phi \to \neg \chi$$
3		ecase33d.3	$$⊢\phi \to \left(\psi \vee \chi \vee \theta \right)$$
4		df-3or	$$⊢\left(\psi \vee \chi \vee \theta \right)\leftrightarrow \left(\left(\psi \vee \chi \right)\vee \theta \right)$$
5	3 4	sylib	$$⊢\phi \to \left(\left(\psi \vee \chi \right)\vee \theta \right)$$
6		ioran	$$⊢\neg \left(\psi \vee \chi \right)\leftrightarrow \left(\neg \psi \wedge \neg \chi \right)$$
7	1 2 6	sylanbrc	$$⊢\phi \to \neg \left(\psi \vee \chi \right)$$
8	5 7	orcnd	$$⊢\phi \to \theta$$