![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mtp-xor | GIF version |
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 1314. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mpto2 1312, that is, it is exclusive-or df-xor 1266), 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 1312), and rule A5 in [Hitchcock] p. 5 (exclusive-or is expressly used). (Contributed by David A. Wheeler, 2-Mar-2018.) |
Ref | Expression |
---|---|
mtp-xor.1 | ⊢ ¬ φ |
mtp-xor.2 | ⊢ (φ ⊻ ψ) |
Ref | Expression |
---|---|
mtp-xor | ⊢ ψ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mtp-xor.1 | . 2 ⊢ ¬ φ | |
2 | mtp-xor.2 | . . . . 5 ⊢ (φ ⊻ ψ) | |
3 | df-xor 1266 | . . . . 5 ⊢ ((φ ⊻ ψ) ↔ ((φ ∨ ψ) ∧ ¬ (φ ∧ ψ))) | |
4 | 2, 3 | mpbi 133 | . . . 4 ⊢ ((φ ∨ ψ) ∧ ¬ (φ ∧ ψ)) |
5 | 4 | simpli 104 | . . 3 ⊢ (φ ∨ ψ) |
6 | 5 | ori 641 | . 2 ⊢ (¬ φ → ψ) |
7 | 1, 6 | ax-mp 7 | 1 ⊢ ψ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 97 ∨ wo 628 ⊻ wxo 1265 |
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-in2 545 ax-io 629 |
This theorem depends on definitions: df-bi 110 df-xor 1266 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |