Theorem trunanfal

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

Conclusion
\( \vdash \top \barwedge \bot \leftrightarrow \top \)
Proof
l0
df-nan
\( \vdash \top \barwedge \bot \leftrightarrow \neg (\top \wedge \bot) \)
truanfal
\( \vdash \top \wedge \bot \leftrightarrow \bot \)
l2
xchbinx l0 _
\( \vdash \top \barwedge \bot \leftrightarrow \neg \bot \)
notfal
\( \vdash \neg \bot \leftrightarrow \top \)
bitri l2 _