Theorem tru 1541

Description: The truth value ⊤ is provable. (Contributed by Anthony Hart, 13-Oct-2010.)

Assertion

Ref	Expression
tru	⊢ ⊤

Proof of Theorem tru

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2		df-tru 1540	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 231	1 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1535   = wceq 1537  ⊤wtru 1538

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 207  df-tru 1540

This theorem is referenced by:  dftru2  1542  trut  1543  mptru  1544  tbtru  1545  bitru  1546  trud  1547  truan  1548  fal  1551  truorfal  1575  falortru  1576  cadtru  1618  nftru  1802  altru  1805  extru  1975  sbtru  2067  vextru  2724  rextru  3083  rabtru  3705  ss2abi  4090  ab0orv  4406  disjprg  5162  reusv2lem5  5420  rabxfr  5436  reuhyp  5438  euotd  5532  mptexgf  7259  elabrex  7279  elabrexg  7280  caovcl  7644  caovass  7650  caovdi  7669  ectocl  8843  fin1a2lem10  10478  riotaneg  12274  zriotaneg  12756  cshwsexaOLD  14873  eflt  16165  efgi0  19762  efgi1  19763  0frgp  19821  mpomulcn  24910  iundisj2  25603  pige3ALT  26580  tanord1  26597  tanord  26598  logtayl  26720  n0sind  28355  nnsind  28381  iundisj2f  32612  iundisj2fi  32802  ordtconn  33871  tgoldbachgt  34640  nexntru  36370  bj-fal  36536  bj-axd2d  36559  bj-rabtr  36896  bj-rabtrALT  36897  bj-dfid2ALT  37031  bj-finsumval0  37251  wl-impchain-mp-x  37413  wl-impchain-com-1.x  37417  wl-impchain-com-n.m  37422  wl-impchain-a1-x  37426  wl-moteq  37468  ftc1anclem5  37657  lhpexle1  39965  3lexlogpow5ineq2  42012  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  mzpcompact2lem  42707  ifpdfor  43427  ifpim1  43431  ifpnot  43432  ifpid2  43433  ifpim2  43434  uun0.1  44749  uunT1  44751  un10  44759  un01  44760  liminfvalxr  45704  ovn02  46489  rmotru  48536  reutru  48537