Theorem tru 1383

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

Syntax hints:   -> wi 4   A.wal 1377   = wceq 1379   T. wtru 1380

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 1382

This theorem is referenced by:  fal  1386  dftru2  1387  trud  1388  tbtru  1389  bitru  1391  a1tru  1395  truan  1396  truorfal  1408  falortru  1409  truimfal  1412  cadtru  1453  nftru  1609  disjprg  4443  reusv2lem5  4652  rabxfr  4669  reuhyp  4675  euotd  4748  elabrex  6141  caovcl  6451  caovass  6457  caovdi  6476  ectocl  7376  fin1a2lem10  8785  riotaneg  10514  zriotaneg  10970  cshwsexa  12751  eflt  13709  efgi0  16534  efgi1  16535  0frgp  16593  iundisj2  21694  pige3  22643  tanord1  22657  tanord  22658  logtayl  22769  iundisj2f  27122  iundisj2fi  27270  ordtcon  27543  allt  29443  nextnt  29447  wl-impchain-mp-x  29533  wl-impchain-com-1.x  29537  wl-impchain-com-n.m  29542  ftc1anclem5  29671  mzpcompact2lem  30288  elabrexg  31012  uun0.1  32655  uunT1  32657  un10  32665  un01  32666  bj-trut  33252  bj-axd2d  33263  bj-rabtr  33578  bj-rabtrALT  33579  bj-df-v  33664  bj-finsumval0  33735  lhpexle1  34804