ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtpor Unicode version

Theorem mtpor 1425
Description: Modus tollendo ponens (inclusive-or version), aka disjunctive syllogism. This is similar to mtpxor 1426, 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 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.)
Hypotheses
Ref Expression
mtpor.min  |-  -.  ph
mtpor.max  |-  ( ph  \/  ps )
Assertion
Ref Expression
mtpor  |-  ps

Proof of Theorem mtpor
StepHypRef Expression
1 mtpor.min . 2  |-  -.  ph
2 mtpor.max . . 3  |-  ( ph  \/  ps )
32ori 723 . 2  |-  ( -. 
ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    \/ wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 615  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  mtpxor  1426  ordtriexmid  4520
  Copyright terms: Public domain W3C validator