Theorem mtord

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

Hypotheses
mtord.1
\( \vdash \varphi \rightarrow \neg \chi \)
mtord.2
\( \vdash \varphi \rightarrow \neg \theta \)
mtord.3
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \vee \theta \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
l0
mtord.2
\( \vdash \varphi \rightarrow \neg \theta \)
l1
mtord.3
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \vee \theta \)
l2
mtord.1
\( \vdash \varphi \rightarrow \neg \chi \)
pm2.53
\( \vdash \chi \vee \theta \rightarrow \neg \chi \rightarrow \theta \)
syl6ci l1 l2 _
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
mtod l0 _