Theorem
tru
The truth value \( \top \) is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
Conclusion
\( \vdash \top \)
Proof
l0
id
\( \vdash \forall x \, x = x \rightarrow \forall x \, x = x \)
df-tru
\( \vdash \top \leftrightarrow \forall x \, x = x \rightarrow \forall x \, x = x \)
mpbir
l0
_
This is the content in the right pane.