Description: The rule of modus tollens. The rule says, "if ps is not true, and
ph implies ps , then ph must also be not true". Modus
tollens is short for "modus tollendo tollens", a Latin phrase that means
"the mode that by denying denies" - remark in Sanford p. 39. It is
also called denying the consequent. Modus tollens is closely related to
modus ponens ax-mp . Note that this rule is also valid in
intuitionistic logic. Inference associated with con3i . (Contributed by NM, 19-Aug-1993)(Proof shortened by Wolf Lammen, 11-Sep-2013)