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

h1::mt2.1           |- ps
h2::mt2.2           |- (ph -> -. ps)
3:2:con2i           |- (ps -> -. ph)
qed:1,3:ax-mp       |- -. ph

$)