Theorem xorexmid

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

Conclusion
\( \vdash \varphi \veebar \neg \varphi \)
Proof
l0
pm5.19
\( \vdash \neg (\varphi \leftrightarrow \neg \varphi) \)
df-xor
\( \vdash \varphi \veebar \neg \varphi \leftrightarrow \neg (\varphi \leftrightarrow \neg \varphi) \)
mpbir l0 _