Theorem noror

\/ is expressible via -\/. (Contributed by Remi, 26-Oct-2023.) (Proof shortened by Wolf Lammen, 8-Dec-2023.)

Conclusion
\( \vdash \varphi \vee \psi \leftrightarrow (\varphi \mathbin{\overline{\vee}} \psi) \mathbin{\overline{\vee}} (\varphi \mathbin{\overline{\vee}} \psi) \)
Proof
df-nor
l1
con2bii _
\( \vdash \varphi \vee \psi \leftrightarrow \neg (\varphi \mathbin{\overline{\vee}} \psi) \)
nornot
\( \vdash \neg (\varphi \mathbin{\overline{\vee}} \psi) \leftrightarrow (\varphi \mathbin{\overline{\vee}} \psi) \mathbin{\overline{\vee}} (\varphi \mathbin{\overline{\vee}} \psi) \)
bitri l1 _