Theorem tru 1377

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

Syntax hints:   -> wi 4   A.wal 1371   = wceq 1373   T. wtru 1374

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 1376

This theorem is referenced by:  fal  1380  dftru2  1381  mptru  1382  tbtru  1383  bitru  1385  trud  1389  truan  1390  truorfal  1426  falortru  1427  truimfal  1430  nftru  1489  euotd  4300  rabxfr  4518  reuhyp  4520  elabrex  5828  elabrexg  5829  caovcl  6103  caovass  6109  caovdi  6128  ectocl  6691  reef11  12043  mpomulcn  15071  bj-sbimeh  15745  bdtru  15805  bj-nn0suc0  15923