|Description: Modus tollendo ponens
(original exclusive-or version), aka disjunctive
syllogism, one of the five "indemonstrables" in Stoic logic.
says, "if is not true, and either or (exclusively)
are true, then must be true." Today the name "modus tollendo
ponens" often refers to a variant, the inclusive-or version as
in mtp-or 1547. See rule 3 on [Lopez-Astorga] p. 12 (note that the
is the same as mpto2 1543, that is, it is exclusive-or df-xor 1314), rule 3
of [Sanford] p. 39 (where it is not as
clearly stated which kind of "or"
is used but it appears to be in the same sense as mpto2 1543), and rule A5
in [Hitchcock] p. 5 (exclusive-or is
expressly used). (Contributed by
David A. Wheeler, 4-Jul-2016.) (Proof shortened by Wolf Lammen,