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

Theorem mtp-xor 1525
Description: Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, 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 mtp-or 1526. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mpto2 1524, that is, it is exclusive-or df-xor 1296), 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 mpto2 1524), and rule A5 in [Hitchcock] p. 5 (exclusive-or is expressly used). (Contributed by David A. Wheeler, 4-Jul-2016.)
Hypotheses
Ref Expression
mtp-xor.1  |-  -.  ph
mtp-xor.2  |-  ( ph \/_ ps )
Assertion
Ref Expression
mtp-xor  |-  ps

Proof of Theorem mtp-xor
StepHypRef Expression
1 mtp-xor.1 . 2  |-  -.  ph
2 mtp-xor.2 . . . . 5  |-  ( ph \/_ ps )
3 df-xor 1296 . . . . 5  |-  ( (
ph \/_ ps )  <->  -.  ( ph 
<->  ps ) )
42, 3mpbi 199 . . . 4  |-  -.  ( ph 
<->  ps )
5 bicom 191 . . . 4  |-  ( (
ph 
<->  ps )  <->  ( ps  <->  ph ) )
64, 5mtbi 289 . . 3  |-  -.  ( ps 
<-> 
ph )
7 xor3 346 . . 3  |-  ( -.  ( ps  <->  ph )  <->  ( ps  <->  -. 
ph ) )
86, 7mpbi 199 . 2  |-  ( ps  <->  -. 
ph )
91, 8mpbir 200 1  |-  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   \/_wxo 1295
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 177  df-xor 1296
  Copyright terms: Public domain W3C validator