Theorem tru 1442

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 23	. 2 |- ( A. x x = x -> A. x x = x )
2		df-tru 1441	. 2 |- ( T. <-> ( A. x x = x -> A. x x = x ) )
3	1, 2	mpbir 213	1 |- T.

Syntax hints:   -> wi 4   A.wal 1436   = wceq 1438   T. wtru 1439

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 189  df-tru 1441

This theorem is referenced by:  fal  1445  dftru2  1446  trud  1447  tbtru  1448  bitru  1450  a1tru  1454  truan  1455  truorfal  1467  falortru  1468  truimfal  1471  falbitru  1477  cadtru  1519  nftru  1674  disjprg  4417  reusv2lem5  4627  rabxfr  4641  reuhyp  4647  euotd  4719  elabrex  6161  caovcl  6475  caovass  6481  caovdi  6500  ectocl  7437  fin1a2lem10  8841  riotaneg  10588  zriotaneg  11051  cshwsexa  12919  eflt  14164  efgi0  17363  efgi1  17364  0frgp  17422  iundisj2  22494  pige3  23464  tanord1  23478  tanord  23479  logtayl  23597  rabtru  28128  iundisj2f  28196  iundisj2fi  28373  ordtcon  28733  allt  31060  nextnt  31064  bj-trut  31164  bj-axd2d  31174  bj-extru  31222  bj-rabtr  31496  bj-rabtrALT  31497  bj-df-v  31581  bj-finsumval0  31660  wl-impchain-mp-x  31744  wl-impchain-com-1.x  31748  wl-impchain-com-n.m  31753  wl-impchain-a1-x  31757  ftc1anclem5  31941  lhpexle1  33498  mzpcompact2lem  35518  ifpdfor  36034  ifpim1  36038  ifpnot  36039  ifpid2  36040  ifpim2  36041  uun0.1  37032  uunT1  37034  un10  37042  un01  37043  elabrexg  37237  ovn02  38171