Theorem biorfi

The dual of biorf is not biantr but iba (and ibar ). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019.)

Hypothesis
biorfi.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \psi \leftrightarrow \varphi \vee \psi \)
Proof
l0
biorfi.1
\( \vdash \neg \varphi \)
biorf
\( \vdash \neg \varphi \rightarrow (\psi \leftrightarrow \varphi \vee \psi) \)
ax-mp l0 _