Theorem norcom

The connector -\/ is commutative. (Contributed by Remi, 25-Oct-2023.) (Proof shortened by Wolf Lammen, 23-Apr-2024.)

Conclusion
\( \vdash \varphi \mathbin{\overline{\vee}} \psi \leftrightarrow \psi \mathbin{\overline{\vee}} \varphi \)
Proof
l0
df-nor
\( \vdash \varphi \mathbin{\overline{\vee}} \psi \leftrightarrow \neg (\varphi \vee \psi) \)
orcom
\( \vdash \varphi \vee \psi \leftrightarrow \psi \vee \varphi \)
l2
xchbinx l0 _
\( \vdash \varphi \mathbin{\overline{\vee}} \psi \leftrightarrow \neg (\psi \vee \varphi) \)
df-nor
\( \vdash \psi \mathbin{\overline{\vee}} \varphi \leftrightarrow \neg (\psi \vee \varphi) \)
bitr4i l2 _