Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > xorexmid | Structured version Visualization version GIF version |
Description: Exclusive-or variant of the law of the excluded middle (exmid 891). This statement is ancient, going back to at least Stoic logic. This statement does not necessarily hold in intuitionistic logic. (Contributed by David A. Wheeler, 23-Feb-2019.) |
Ref | Expression |
---|---|
xorexmid | ⊢ (𝜑 ⊻ ¬ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.19 390 | . 2 ⊢ ¬ (𝜑 ↔ ¬ 𝜑) | |
2 | df-xor 1502 | . 2 ⊢ ((𝜑 ⊻ ¬ 𝜑) ↔ ¬ (𝜑 ↔ ¬ 𝜑)) | |
3 | 1, 2 | mpbir 233 | 1 ⊢ (𝜑 ⊻ ¬ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 208 ⊻ wxo 1501 |
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 209 df-xor 1502 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |