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 φ ¬ ψ