Theorem noran

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

Conclusion
\( \vdash \varphi \wedge \psi \leftrightarrow (\varphi \mathbin{\overline{\vee}} \varphi) \mathbin{\overline{\vee}} (\psi \mathbin{\overline{\vee}} \psi) \)
Proof
l0
anor
\( \vdash \varphi \wedge \psi \leftrightarrow \neg (\neg \varphi \vee \neg \psi) \)
l1
nornot
nornot
orbi12i l1 _
\( \vdash \neg \varphi \vee \neg \psi \leftrightarrow \varphi \mathbin{\overline{\vee}} \varphi \vee (\psi \mathbin{\overline{\vee}} \psi) \)
l4
xchbinx l0 _
\( \vdash \varphi \wedge \psi \leftrightarrow \neg (\varphi \mathbin{\overline{\vee}} \varphi \vee (\psi \mathbin{\overline{\vee}} \psi)) \)
df-nor
\( \vdash (\varphi \mathbin{\overline{\vee}} \varphi) \mathbin{\overline{\vee}} (\psi \mathbin{\overline{\vee}} \psi) \leftrightarrow \neg (\varphi \mathbin{\overline{\vee}} \varphi \vee (\psi \mathbin{\overline{\vee}} \psi)) \)
bitr4i l4 _