Theorem nornot

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

Conclusion
\( \vdash \neg \varphi \leftrightarrow \varphi \mathbin{\overline{\vee}} \varphi \)
Proof
l0
df-nor
\( \vdash \varphi \mathbin{\overline{\vee}} \varphi \leftrightarrow \neg (\varphi \vee \varphi) \)
oridm
\( \vdash \varphi \vee \varphi \leftrightarrow \varphi \)
xchbinx l0 _
bicomi _