MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtp-or Structured version   Unicode version

Theorem mtp-or 1548
Description: Modus tollendo ponens (inclusive-or version), aka disjunctive syllogism. This is similar to mtp-xor 1546, 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  ph is not true, and  ph or  ps (or both) are true, then  ps must be true." An alternative 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.)
Hypotheses
Ref Expression
mtp-or.1  |-  -.  ph
mtp-or.2  |-  ( ph  \/  ps )
Assertion
Ref Expression
mtp-or  |-  ps

Proof of Theorem mtp-or
StepHypRef Expression
1 mtp-or.1 . 2  |-  -.  ph
2 mtp-or.2 . . 3  |-  ( ph  \/  ps )
32ori 366 . 2  |-  ( -. 
ph  ->  ps )
41, 3ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 359
This theorem is referenced by:  tfrlem14  6654  cardom  7875  unialeph  7984  brdom3  8408  sinhalfpilem  20376  mof  26162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator