Theorem biorfri

A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.) (Proof shortened by AV, 10-Aug-2025.)

Hypothesis
biorfi.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \psi \leftrightarrow \psi \vee \varphi \)
Proof
biorfi.1
l1
biorfi _
\( \vdash \psi \leftrightarrow \varphi \vee \psi \)
orcom
\( \vdash \varphi \vee \psi \leftrightarrow \psi \vee \varphi \)
bitri l1 _