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

Metamath Proof Explorer

Theorem mtoi

Description: Modus tollens inference. (Contributed by NM, 5-Jul-1994) (Proof shortened by Wolf Lammen, 15-Sep-2012)

Ref Expression
Hypotheses mtoi.1 ⊢ ¬ χ
mtoi.2 ⊢ φ → ψ → χ
Assertion mtoi ⊢ φ → ¬ ψ

Proof

Step Hyp Ref Expression
1 mtoi.1 ⊢ ¬ χ
2 mtoi.2 ⊢ φ → ψ → χ
3 1 a1i ⊢ φ → ¬ χ
4 3 2 mtod ⊢ φ → ¬ ψ