$( <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
⊢
¬
φ
$)