Theorem xorneg

The connector \/_ is unchanged under negation of both arguments. (Contributed by Mario Carneiro, 4-Sep-2016.)

Conclusion
\( \vdash \neg \varphi \veebar \neg \psi \leftrightarrow \varphi \veebar \psi \)
Proof
l0
xorneg1
\( \vdash \neg \varphi \veebar \neg \psi \leftrightarrow \neg (\varphi \veebar \neg \psi) \)
xorneg2
con2bii _
\( \vdash \varphi \veebar \psi \leftrightarrow \neg (\varphi \veebar \neg \psi) \)
bitr4i l0 _