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

Theorem mtp-xor 1530
 Description: Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, one of the five "indemonstrables" in Stoic logic. The rule says, "if is not true, and either or (exclusively) are true, then must be true." Today the name "modus tollendo ponens" often refers to a variant, the inclusive-or version as defined in mtp-or 1531. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mpto2 1529, that is, it is exclusive-or df-xor 1301), 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 1529), 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
mtp-xor.2
Assertion
Ref Expression
mtp-xor

Proof of Theorem mtp-xor
StepHypRef Expression
1 mtp-xor.1 . 2
2 mtp-xor.2 . . . . 5
3 df-xor 1301 . . . . 5
42, 3mpbi 201 . . . 4
5 bicom 193 . . . 4
64, 5mtbi 291 . . 3
7 xor3 348 . . 3
86, 7mpbi 201 . 2
91, 8mpbir 202 1
 Colors of variables: wff set class Syntax hints:   wn 5   wb 178  wxo 1300 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10 This theorem depends on definitions:  df-bi 179  df-xor 1301
 Copyright terms: Public domain W3C validator