Theorem
biortn
A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \neg \varphi \vee \psi) \)
Proof
l0
notnot
\( \vdash \varphi \rightarrow \neg \neg \varphi \)
biorf
\( \vdash \neg \neg \varphi \rightarrow (\psi \leftrightarrow \neg \varphi \vee \psi) \)
syl
l0
_
This is the content in the right pane.