Theorem xorexmid 1557

Description: Exclusive-or variant of the law of the excluded middle (exmid 908). 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 391	. 2 ⊢ ¬ (𝜑 ↔ ¬ 𝜑)
2		df-xor 1542	. 2 ⊢ ((𝜑 ⊻ ¬ 𝜑) ↔ ¬ (𝜑 ↔ ¬ 𝜑))
3	1, 2	mpbir 234	1 ⊢ (𝜑 ⊻ ¬ 𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ⊻ wxo 1541

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-xor 1542

This theorem is used by: (None)