Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mtpxor Unicode version

Theorem mtpxor 1317
 Description: Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, similar to mtpor 1316, 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 mtpor 1316. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mptxor 1315, that is, it is exclusive-or df-xor 1267), 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 1315), 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
mtpxor.maj
Assertion
Ref Expression
mtpxor

Proof of Theorem mtpxor
StepHypRef Expression
1 mtpxor.min . 2
2 mtpxor.maj . . 3
3 xoror 1270 . . 3
42, 3ax-mp 7 . 2
51, 4mtpor 1316 1
 Colors of variables: wff set class Syntax hints:   wn 3   wo 629   wxo 1266 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630 This theorem depends on definitions:  df-bi 110  df-xor 1267 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator