Theorem mtpor 1695

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

Assertion

Ref	Expression
mtpor	|- ps

Proof of Theorem mtpor

Step	Hyp	Ref	Expression
1		mtpor.min	. 2 |- -. ph
2		mtpor.max	. . 3 |- ( ph \/ ps )
3	2	ori 390	. 2 |- ( -. ph -> ps )
4	1, 3	ax-mp 5	1 |- ps

Syntax hints:   -. wn 3   \/ wo 383

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 197  df-or 385

This theorem is referenced by:  mtpxor  1696  tfrlem14  7487  cardom  8812  unialeph  8924  brdom3  9350  sinhalfpilem  24215  mof  32409  dvnprodlem3  40163