Theorem xorneg1

The connector \/_ is negated under negation of one argument. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 27-Jun-2020.)

Conclusion
\( \vdash \neg \varphi \veebar \psi \leftrightarrow \neg (\varphi \veebar \psi) \)
Proof
l0
xorcom
\( \vdash \neg \varphi \veebar \psi \leftrightarrow \psi \veebar \neg \varphi \)
l1
xorneg2
\( \vdash \psi \veebar \neg \varphi \leftrightarrow \neg (\psi \veebar \varphi) \)
xorcom
\( \vdash \psi \veebar \varphi \leftrightarrow \varphi \veebar \psi \)
xchbinx l1 _
\( \vdash \psi \veebar \neg \varphi \leftrightarrow \neg (\varphi \veebar \psi) \)
bitri l0 _