Theorem mtpxor 1604

Description: Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, similar to mtpor 1603, 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 1603. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mptxor 1602, that is, it is exclusive-or df-xor 1364), 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 1602), 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

Step	Hyp	Ref	Expression
1		mtpxor.min	. 2
2		mtpxor.maj	. . 3
3		xoror 1370	. . 3
4	2, 3	ax-mp 5	. 2
5	1, 4	mtpor 1603	1

Syntax hints:  -.wn 3  \/wo 368  \/_wxo 1363

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 1364