Theorem tbw-bijust

Justification for tbw-negdf. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot \)
Proof
l0
dfbi1
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \)
pm2.21
l2
imim2i _
l3
id
falim
ja l3 _
imim2i _
impbii l2 _
l8
notbii _
\( \vdash \neg ((\varphi \rightarrow \psi) \rightarrow \neg (\psi \rightarrow \varphi)) \leftrightarrow \neg ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \bot) \)
l9
pm2.21
l10
ax-1
falim
ja l10 _
pm2.43i _
impbii l9 _
\( \vdash \neg ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \bot) \leftrightarrow ((\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \varphi) \rightarrow \bot) \rightarrow \bot \)
3bitri l0 l8 _