Theorem tru 1373

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

Syntax hints:   -> wi 4   A.wal 1367   = wceq 1369   T. wtru 1370

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 1372

This theorem is referenced by:  fal  1376  dftru2  1377  trud  1378  tbtru  1379  bitru  1381  a1tru  1385  truan  1386  truorfal  1398  falortru  1399  truimfal  1402  cadtru  1443  nftru  1599  disjprg  4288  reusv2lem5  4497  rabxfr  4514  reuhyp  4520  euotd  4592  elabrex  5960  caovcl  6257  caovass  6263  caovdi  6282  ectocl  7168  fin1a2lem10  8578  riotaneg  10305  zriotaneg  10754  cshwsexa  12458  eflt  13401  efgi0  16217  efgi1  16218  0frgp  16276  iundisj2  21030  pige3  21979  tanord1  21993  tanord  21994  logtayl  22105  colperp  23114  iundisj2f  25932  iundisj2fi  26081  ordtcon  26355  allt  28247  nextnt  28251  ftc1anclem5  28471  mzpcompact2lem  29088  uun0.1  31511  uunT1  31513  un10  31521  un01  31522  bj-trut  32108  bj-axd2d  32128  bj-rabtr  32432  bj-rabtrALT  32433  bj-finsumval0  32583  lhpexle1  33652