Metamath Proof Explorer

Theorem tru

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

Ref Expression
Assertion tru 
|- T.

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A. x x = x -> A. x x = x )
2 df-tru 
 |-  ( T. <-> ( A. x x = x -> A. x x = x ) )
3 1 2 mpbir 
 |-  T.