Theorem falnantru

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

Conclusion
\( \vdash \bot \barwedge \top \leftrightarrow \top \)
Proof
l0
nancom
\( \vdash \bot \barwedge \top \leftrightarrow \top \barwedge \bot \)
trunanfal
\( \vdash \top \barwedge \bot \leftrightarrow \top \)
bitri l0 _