Theorem tru 1335

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

Syntax hints:   -> wi 4   A.wal 1329   = wceq 1331   T. wtru 1332

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 1334

This theorem is referenced by:  fal  1338  dftru2  1339  mptru  1340  tbtru  1341  bitru  1343  a1tru  1347  truan  1348  truorfal  1384  falortru  1385  truimfal  1388  nftru  1442  euotd  4176  rabxfr  4391  reuhyp  4393  elabrex  5659  caovcl  5925  caovass  5931  caovdi  5950  ectocl  6496  reef11  11406  bj-sbimeh  12979  bdtru  13030  bj-nn0suc0  13148