Theorem falnorfal

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

Conclusion
\( \vdash \bot \mathbin{\overline{\vee}} \bot \leftrightarrow \top \)
Proof
l0
df-nor
\( \vdash \bot \mathbin{\overline{\vee}} \bot \leftrightarrow \neg (\bot \vee \bot) \)
falorfal
\( \vdash \bot \vee \bot \leftrightarrow \bot \)
l2
xchbinx l0 _
\( \vdash \bot \mathbin{\overline{\vee}} \bot \leftrightarrow \neg \bot \)
notfal
\( \vdash \neg \bot \leftrightarrow \top \)
bitri l2 _