Theorem norasslem2

This lemma specializes biimt suitably for the proof of norass. (Contributed by Wolf Lammen, 18-Dec-2023.)

Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi \vee \chi \rightarrow \psi) \)
Proof
biimt
\( \vdash \varphi \vee \chi \rightarrow (\psi \leftrightarrow \varphi \vee \chi \rightarrow \psi) \)
orcs _