Theorem mtpxor 1421

Description: Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, similar to mtpor 1420, 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 mtpor 1420. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mptxor 1419, that is, it is exclusive-or df-xor 1371), 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 1419), 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	|- -. ph
mtpxor.maj	|- ( ph \/_ ps )

Assertion

Ref	Expression
mtpxor	|- ps

Proof of Theorem mtpxor

Step	Hyp	Ref	Expression
1		mtpxor.min	. 2 |- -. ph
2		mtpxor.maj	. . 3 |- ( ph \/_ ps )
3		xoror 1374	. . 3 |- ( ( ph \/_ ps ) -> ( ph \/ ps ) )
4	2, 3	ax-mp 5	. 2 |- ( ph \/ ps )
5	1, 4	mtpor 1420	1 |- ps

Syntax hints:   -. wn 3   \/ wo 703   \/_ wxo 1370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704

This theorem depends on definitions:  df-bi 116  df-xor 1371

This theorem is referenced by: (None)