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

Metamath Proof Explorer

Theorem mt3i

Description: Modus tollens inference. (Contributed by NM, 26-Mar-1995) (Proof shortened by Wolf Lammen, 15-Sep-2012)

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

Proof

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