This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mtord

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

Ref Expression
Hypotheses mtord.1 ⊢ φ → ¬ χ
mtord.2 ⊢ φ → ¬ θ
mtord.3 ⊢ φ → ψ → χ ∨ θ
Assertion mtord ⊢ φ → ¬ ψ

Proof

Step Hyp Ref Expression
1 mtord.1 ⊢ φ → ¬ χ
2 mtord.2 ⊢ φ → ¬ θ
3 mtord.3 ⊢ φ → ψ → χ ∨ θ
4 pm2.53 ⊢ χ ∨ θ → ¬ χ → θ
5 3 1 4 syl6ci ⊢ φ → ψ → θ
6 2 5 mtod ⊢ φ → ¬ ψ