Theorem orcanai

Description: Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994)

	Ref	Expression
Hypothesis	orcanai.1	$$⊢\phi \to \left(\psi \vee \chi \right)$$
Assertion	orcanai	$$⊢\left(\phi \wedge \neg \psi \right)\to \chi$$

Proof

Step	Hyp	Ref	Expression
1		orcanai.1	$$⊢\phi \to \left(\psi \vee \chi \right)$$
2	1	ord	$$⊢\phi \to \left(\neg \psi \to \chi \right)$$
3	2	imp	$$⊢\left(\phi \wedge \neg \psi \right)\to \chi$$