Theorem mtp-xor 1536

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 1538. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mpto2 1534, that is, it is exclusive-or df-xor 1305), 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 1534), 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.)

Hypotheses

Ref	Expression
mtp-xor.1	|- -. ph
mtp-xor.2	|- (ph \/_ ps)

Assertion

Ref	Expression
mtp-xor	|- ps

Proof of Theorem mtp-xor

Step	Hyp	Ref	Expression
1		mtp-xor.1	. . 3 |- -. ph
2		mtp-xor.2	. . . 4 |- (ph \/_ ps)
3		xorneg 1313	. . . 4 |- ((-. ph \/_ -. ps) <-> (ph \/_ ps))
4	2, 3	mpbir 200	. . 3 |- (-. ph \/_ -. ps)
5	1, 4	mpto2 1534	. 2 |- -. -. ps
6	5	notnotri 106	1 |- ps

Syntax hints:  -. wn 3   \/_ wxo 1304

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 177  df-xor 1305

This theorem is referenced by: (None)