Theorem tru 1448

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

Syntax hints:   -> wi 4   A.wal 1442   = wceq 1444   T. wtru 1445

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 1447

This theorem is referenced by:  fal  1451  dftru2  1452  trud  1453  tbtru  1454  bitru  1456  a1tru  1460  truan  1461  truorfal  1471  falortru  1472  truimfal  1475  falbitru  1481  cadtru  1523  nftru  1677  disjprg  4398  reusv2lem5  4608  rabxfr  4622  reuhyp  4628  euotd  4702  elabrex  6148  caovcl  6463  caovass  6469  caovdi  6488  ectocl  7431  fin1a2lem10  8839  riotaneg  10586  zriotaneg  11049  cshwsexa  12923  eflt  14171  efgi0  17370  efgi1  17371  0frgp  17429  iundisj2  22502  pige3  23472  tanord1  23486  tanord  23487  logtayl  23605  rabtru  28135  iundisj2f  28200  iundisj2fi  28373  ordtcon  28731  allt  31061  nextnt  31065  bj-trut  31166  bj-axd2d  31176  bj-nftru  31199  bj-extru  31267  bj-rabtr  31533  bj-rabtrALT  31534  bj-rabtrALTALT  31535  bj-df-v  31620  bj-finsumval0  31702  wl-impchain-mp-x  31824  wl-impchain-com-1.x  31828  wl-impchain-com-n.m  31833  wl-impchain-a1-x  31837  ftc1anclem5  32021  lhpexle1  33573  mzpcompact2lem  35593  ifpdfor  36108  ifpim1  36112  ifpnot  36113  ifpid2  36114  ifpim2  36115  uun0.1  37165  uunT1  37167  un10  37175  un01  37176  elabrexg  37370  ovn02  38390