Theorem tru 1293

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

Assertion

Ref	Expression
tru	|- T.

Proof of Theorem tru

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

Syntax hints:   -> wi 4   A.wal 1287   = wceq 1289   T. wtru 1290

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-tru 1292

This theorem is referenced by:  fal  1296  dftru2  1297  mptru  1298  tbtru  1299  bitru  1301  a1tru  1305  truan  1306  truorfal  1342  falortru  1343  truimfal  1346  nftru  1400  euotd  4081  rabxfr  4292  reuhyp  4294  elabrex  5537  caovcl  5799  caovass  5805  caovdi  5824  ectocl  6359  reef11  10990  bj-sbimeh  11673  bdtru  11723  bj-nn0suc0  11845