Theorem mtord

Description: A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009)

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

Proof

Step	Hyp	Ref	Expression
1		mtord.1	$$⊢\phi \to \neg \chi$$
2		mtord.2	$$⊢\phi \to \neg \theta$$
3		mtord.3	$$⊢\phi \to \left(\psi \to \left(\chi \vee \theta \right)\right)$$
4		pm2.53	$$⊢\left(\chi \vee \theta \right)\to \left(\neg \chi \to \theta \right)$$
5	3 1 4	syl6ci	$$⊢\phi \to \left(\psi \to \theta \right)$$
6	2 5	mtod	$$⊢\phi \to \neg \psi$$