Theorem tru 1411

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

Syntax hints:   -> wi 4   A.wal 1405   = wceq 1407   T. wtru 1408

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 187  df-tru 1410

This theorem is referenced by:  fal  1414  dftru2  1415  trud  1416  tbtru  1417  bitru  1419  a1tru  1423  truan  1424  truorfal  1436  falortru  1437  truimfal  1440  falbitru  1446  cadtru  1490  nftru  1649  disjprg  4393  reusv2lem5  4601  rabxfr  4615  reuhyp  4621  euotd  4693  elabrex  6138  caovcl  6452  caovass  6458  caovdi  6477  ectocl  7418  fin1a2lem10  8823  riotaneg  10560  zriotaneg  11019  cshwsexa  12850  eflt  14063  efgi0  17064  efgi1  17065  0frgp  17123  iundisj2  22253  pige3  23204  tanord1  23218  tanord  23219  logtayl  23337  rabtru  27827  iundisj2f  27895  iundisj2fi  28063  ordtcon  28373  allt  30646  nextnt  30650  bj-trut  30748  bj-axd2d  30758  bj-rabtr  31075  bj-rabtrALT  31076  bj-df-v  31161  bj-finsumval0  31240  wl-impchain-mp-x  31324  wl-impchain-com-1.x  31328  wl-impchain-com-n.m  31333  wl-impchain-a1-x  31337  ftc1anclem5  31480  lhpexle1  33038  mzpcompact2lem  35058  ifpdfor  35568  ifpim1  35572  ifpnot  35573  ifpid2  35574  ifpim2  35575  uun0.1  36612  uunT1  36614  un10  36622  un01  36623  elabrexg  36819