Theorem tru 1387

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 22	. 2 |- ( A. x x = x -> A. x x = x )
2		df-tru 1386	. 2 |- ( T. <-> ( A. x x = x -> A. x x = x ) )
3	1, 2	mpbir 209	1 |- T.

Syntax hints:   -> wi 4   A.wal 1381   = wceq 1383   T. wtru 1384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-tru 1386

This theorem is referenced by:  fal  1390  dftru2  1391  trud  1392  tbtru  1393  bitru  1395  a1tru  1399  truan  1400  truorfal  1412  falortru  1413  truimfal  1416  cadtru  1456  nftru  1613  disjprg  4433  reusv2lem5  4642  rabxfr  4659  reuhyp  4665  euotd  4738  elabrex  6140  caovcl  6454  caovass  6460  caovdi  6479  ectocl  7381  fin1a2lem10  8792  riotaneg  10525  zriotaneg  10984  cshwsexa  12774  eflt  13834  efgi0  16717  efgi1  16718  0frgp  16776  iundisj2  21937  pige3  22888  tanord1  22902  tanord  22903  logtayl  23019  iundisj2f  27427  iundisj2fi  27580  ordtcon  27885  allt  29842  nextnt  29846  wl-impchain-mp-x  29932  wl-impchain-com-1.x  29936  wl-impchain-com-n.m  29941  ftc1anclem5  30070  mzpcompact2lem  30660  elabrexg  31384  etransclem46  32017  uun0.1  33443  uunT1  33445  un10  33453  un01  33454  bj-trut  34054  bj-axd2d  34064  bj-rabtr  34380  bj-rabtrALT  34381  bj-df-v  34466  bj-finsumval0  34538  lhpexle1  35607