Theorem falxortru

A \/_ identity. (Contributed by David A. Wheeler, 9-May-2015.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)

Conclusion
\( \vdash \bot \veebar \top \leftrightarrow \top \)
Proof
l0
xorcom
\( \vdash \bot \veebar \top \leftrightarrow \top \veebar \bot \)
truxorfal
\( \vdash \top \veebar \bot \leftrightarrow \top \)
bitri l0 _