Theorem xorneg2

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 \varphi \veebar \neg \psi \leftrightarrow \neg (\varphi \veebar \psi) \)
Proof
l0
df-xor
\( \vdash \varphi \veebar \neg \psi \leftrightarrow \neg (\varphi \leftrightarrow \neg \psi) \)
l1
pm5.18
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg (\varphi \leftrightarrow \neg \psi) \)
xnor
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg (\varphi \veebar \psi) \)
3bitr2i l0 l1 _