Metamath Proof Explorer


Theorem mtand

Description: A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009)

Ref Expression
Hypotheses mtand.1 φ ¬ χ
mtand.2 φ ψ χ
Assertion mtand φ ¬ ψ

Proof

Step Hyp Ref Expression
1 mtand.1 φ ¬ χ
2 mtand.2 φ ψ χ
3 2 ex φ ψ χ
4 1 3 mtod φ ¬ ψ