Theorem trubifal

A <-> identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)

Conclusion
\( \vdash \top \leftrightarrow \bot \leftrightarrow \bot \)
Proof
l0
bicom
\( \vdash \top \leftrightarrow \bot \leftrightarrow (\bot \leftrightarrow \top) \)
falbitru
\( \vdash \bot \leftrightarrow \top \leftrightarrow \bot \)
bitri l0 _