Theorem norasslem1

This lemma shows the equivalence of two expressions, used in norass. (Contributed by Wolf Lammen, 18-Dec-2023.)

Conclusion
\( \vdash \varphi \vee \psi \rightarrow \chi \leftrightarrow \varphi \mathbin{\overline{\vee}} \psi \vee \chi \)
Proof
l0
imor
\( \vdash \varphi \vee \psi \rightarrow \chi \leftrightarrow \neg (\varphi \vee \psi) \vee \chi \)
df-nor
orbi1i _
\( \vdash \varphi \mathbin{\overline{\vee}} \psi \vee \chi \leftrightarrow \neg (\varphi \vee \psi) \vee \chi \)
bitr4i l0 _