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

Theorem mtpxor 1579
Description: Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, similar to mtpor 1578, one of the five "indemonstrables" in Stoic logic. The rule says, "if  ph is not true, and either  ph or  ps (exclusively) are true, then  ps must be true." Today the name "modus tollendo ponens" often refers to a variant, the inclusive-or version as defined in mtpor 1578. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mptxor 1577, that is, it is exclusive-or df-xor 1352), rule 3 of [Sanford] p. 39 (where it is not as clearly stated which kind of "or" is used but it appears to be in the same sense as mptxor 1577), and rule A5 in [Hitchcock] p. 5 (exclusive-or is expressly used). (Contributed by David A. Wheeler, 4-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.) (Proof shortened by BJ, 19-Apr-2019.)
Hypotheses
Ref Expression
mtpxor.min  |-  -.  ph
mtpxor.maj  |-  ( ph  \/_ 
ps )
Assertion
Ref Expression
mtpxor  |-  ps

Proof of Theorem mtpxor
StepHypRef Expression
1 mtpxor.min . 2  |-  -.  ph
2 mtpxor.maj . . 3  |-  ( ph  \/_ 
ps )
3 xoror 1358 . . 3  |-  ( (
ph  \/_  ps )  ->  ( ph  \/  ps ) )
42, 3ax-mp 5 . 2  |-  ( ph  \/  ps )
51, 4mtpor 1578 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    \/ wo 368    \/_ wxo 1351
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 185  df-or 370  df-an 371  df-xor 1352
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator