$( <MM> <PROOF ASST> THEOREM= mt2  LOC_AFTER= mt2
 
* A rule similar to modus tollens.

h1::mt2.1           ψ
h2::mt2.2           (φ → ¬ ψ)
3:2:con2i           (ψ → ¬ φ)
qed:1,3:ax-mp       ¬ φ

$)