Theorem tru 1336

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 1335	. 2 |- ( T. <-> ( A. x x = x -> A. x x = x ) )
3	1, 2	mpbir 145	1 |- T.

Syntax hints:   -> wi 4   A.wal 1330   = wceq 1332   T. wtru 1333

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

This theorem depends on definitions:  df-bi 116  df-tru 1335

This theorem is referenced by:  fal  1339  dftru2  1340  mptru  1341  tbtru  1342  bitru  1344  a1tru  1348  truan  1349  truorfal  1385  falortru  1386  truimfal  1389  nftru  1443  euotd  4184  rabxfr  4399  reuhyp  4401  elabrex  5667  caovcl  5933  caovass  5939  caovdi  5958  ectocl  6504  reef11  11442  bj-sbimeh  13150  bdtru  13201  bj-nn0suc0  13319