Theorem xorexmid 1521

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.)

Assertion

Ref	Expression
xorexmid	⊢ (𝜑 ⊻ ¬ 𝜑)

Proof of Theorem xorexmid

Step	Hyp	Ref	Expression
1		pm5.19 387	. 2 ⊢ ¬ (𝜑 ↔ ¬ 𝜑)
2		df-xor 1504	. 2 ⊢ ((𝜑 ⊻ ¬ 𝜑) ↔ ¬ (𝜑 ↔ ¬ 𝜑))
3	1, 2	mpbir 230	1 ⊢ (𝜑 ⊻ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 205   ⊻ wxo 1503

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 206  df-xor 1504

This theorem is referenced by: (None)