Theorem tru

Description: The truth value T. is provable. (Contributed by Anthony Hart, 13-Oct-2010)

	Ref	Expression
Assertion	tru	$$⊢\top$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\forall xx=x\to \forall xx=x$$
2		df-tru	$$⊢\top \leftrightarrow \left(\forall xx=x\to \forall xx=x\right)$$
3	1 2	mpbir	$$⊢\top$$