Theorem trunantru

A -/\ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Conclusion
\( \vdash \top \barwedge \top \leftrightarrow \bot \)
Proof
l0
nannot
\( \vdash \neg \top \leftrightarrow \top \barwedge \top \)
nottru
\( \vdash \neg \top \leftrightarrow \bot \)
bitr3i l0 _