Theorem trunortru

A -\/ identity. (Contributed by Remi, 25-Oct-2023.) (Proof shortened by Wolf Lammen, 7-Dec-2023.)

Conclusion
\( \vdash \top \mathbin{\overline{\vee}} \top \leftrightarrow \bot \)
Proof
l0
df-nor
\( \vdash \top \mathbin{\overline{\vee}} \top \leftrightarrow \neg (\top \vee \top) \)
truortru
\( \vdash \top \vee \top \leftrightarrow \top \)
l2
xchbinx l0 _
\( \vdash \top \mathbin{\overline{\vee}} \top \leftrightarrow \neg \top \)
df-fal
\( \vdash \bot \leftrightarrow \neg \top \)
bitr4i l2 _