Theorem truxorfal

A \/_ identity. (Contributed by David A. Wheeler, 8-May-2015.)

Conclusion
\( \vdash \top \veebar \bot \leftrightarrow \top \)
Proof
l0
df-xor
\( \vdash \top \veebar \bot \leftrightarrow \neg (\top \leftrightarrow \bot) \)
trubifal
\( \vdash \top \leftrightarrow \bot \leftrightarrow \bot \)
l2
xchbinx l0 _
\( \vdash \top \veebar \bot \leftrightarrow \neg \bot \)
notfal
\( \vdash \neg \bot \leftrightarrow \top \)
bitri l2 _