Theorem rb-bijust

Justification for rb-imdf. (Contributed by Anthony Hart, 17-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
Proof
l0
dfbi1
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \)
l1
imor
imor
notbii _
imbi12i l1 _
l5
notbii _
\( \vdash \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \leftrightarrow \neg (\neg \varphi \vee \psi \rightarrow \neg (\neg \psi \vee \varphi)) \)
pm4.62
notbii _
\( \vdash \neg (\neg \varphi \vee \psi \rightarrow \neg (\neg \psi \vee \varphi)) \leftrightarrow \neg (\neg (\neg \varphi \vee \psi) \vee \neg (\neg \psi \vee \varphi)) \)
3bitri l0 l5 _