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