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		3orass	$$⊢\left(\psi \vee \chi \vee \theta \right)\leftrightarrow \left(\psi \vee \left(\chi \vee \theta \right)\right)$$
5	3 4	sylib	$$⊢\phi \to \left(\psi \vee \left(\chi \vee \theta \right)\right)$$
6		ioran	$$⊢\neg \left(\chi \vee \theta \right)\leftrightarrow \left(\neg \chi \wedge \neg \theta \right)$$
7	1 2 6	sylanbrc	$$⊢\phi \to \neg \left(\chi \vee \theta \right)$$
8	5 7	olcnd	$$⊢\phi \to \psi$$