Theorem biorf

A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)

Conclusion
\( \vdash \neg \varphi \rightarrow (\psi \leftrightarrow \varphi \vee \psi) \)
Proof
l0
olc
orel1
impbid2 l0 _