Theorem tru 1368

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

Syntax hints:   -> wi 4   A.wal 1362   = wceq 1364   T. wtru 1365

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

This theorem depends on definitions:  df-bi 117  df-tru 1367

This theorem is referenced by:  fal  1371  dftru2  1372  mptru  1373  tbtru  1374  bitru  1376  trud  1380  truan  1381  truorfal  1417  falortru  1418  truimfal  1421  nftru  1477  euotd  4284  rabxfr  4502  reuhyp  4504  elabrex  5801  elabrexg  5802  caovcl  6075  caovass  6081  caovdi  6100  ectocl  6658  reef11  11845  mpomulcn  14745  bj-sbimeh  15334  bdtru  15394  bj-nn0suc0  15512