Modus tollendo ponens (inclusive-or version), aka disjunctive syllogism. This is similar to mtpxor, one of the five original "indemonstrables" in Stoic logic. However, in Stoic logic this rule used exclusive-or, while the name modus tollendo ponens often refers to a variant of the rule that uses inclusive-or instead. The rule says, "if \( \varphi \) is not true, and \( \varphi \) or \( \psi \) (or both) are true, then \( \psi \) must be true". An alternate phrasing is: "once you eliminate the impossible, whatever remains, no matter how improbable, must be the truth". -- Sherlock Holmes (Sir Arthur Conan Doyle, 1890: The Sign of the Four, ch. 6). (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.)