Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mtpor Structured version   Visualization version   Unicode version

Theorem mtpor 1655
 Description: Modus tollendo ponens (inclusive-or version), aka disjunctive syllogism. This is similar to mtpxor 1656, 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 is not true, and or (or both) are true, then 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
mtpor.min
mtpor.max
Assertion
Ref Expression
mtpor

Proof of Theorem mtpor
StepHypRef Expression
1 mtpor.min . 2
2 mtpor.max . . 3
32ori 377 . 2
41, 3ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wo 370 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 189  df-or 372 This theorem is referenced by:  mtpxor  1656  tfrlem14  7114  cardom  8425  unialeph  8537  brdom3  8961  sinhalfpilem  23430  mof  31082  dvnprodlem3  37833
 Copyright terms: Public domain W3C validator