Theorem ecase23d

Description: Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994)

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

Proof

Step	Hyp	Ref	Expression
1		ecase23d.1	$$⊢\phi \to \neg \chi$$
2		ecase23d.2	$$⊢\phi \to \neg \theta$$
3		ecase23d.3	$$⊢\phi \to \left(\psi \vee \chi \vee \theta \right)$$
4		ioran	$$⊢\neg \left(\chi \vee \theta \right)\leftrightarrow \left(\neg \chi \wedge \neg \theta \right)$$
5	1 2 4	sylanbrc	$$⊢\phi \to \neg \left(\chi \vee \theta \right)$$
6		3orass	$$⊢\left(\psi \vee \chi \vee \theta \right)\leftrightarrow \left(\psi \vee \left(\chi \vee \theta \right)\right)$$
7	3 6	sylib	$$⊢\phi \to \left(\psi \vee \left(\chi \vee \theta \right)\right)$$
8	7	ord	$$⊢\phi \to \left(\neg \psi \to \left(\chi \vee \theta \right)\right)$$
9	5 8	mt3d	$$⊢\phi \to \psi$$