$( <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
$)