Metamath Proof Explorer

Theorem xorexmid

Description: Exclusive-or variant of the law of the excluded middle ( exmid ). 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
Assertion xorexmid φ ¬ φ


Step Hyp Ref Expression
1 pm5.19 ¬ φ ¬ φ
2 df-xor φ ¬ φ ¬ φ ¬ φ
3 1 2 mpbir φ ¬ φ