Theorem tru 1544

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 1543	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 231	1 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1538   = wceq 1540  ⊤wtru 1541

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 1543

This theorem is referenced by:  dftru2  1545  trut  1546  mptru  1547  tbtru  1548  bitru  1549  trud  1550  truan  1551  fal  1554  truorfal  1578  falortru  1579  cadtru  1620  nftru  1804  altru  1807  extru  1975  sbtru  2068  vextru  2714  rextru  3060  rabtru  3656  ss2abi  4030  ab0orv  4346  disjprg  5103  reusv2lem5  5357  rabxfr  5373  reuhyp  5375  euotd  5473  mptexgf  7196  elabrex  7216  elabrexg  7217  caovcl  7583  caovass  7589  caovdi  7608  ectocl  8756  fin1a2lem10  10362  riotaneg  12162  zriotaneg  12647  cshwsexaOLD  14790  eflt  16085  efgi0  19650  efgi1  19651  0frgp  19709  mpomulcn  24758  iundisj2  25450  pige3ALT  26429  tanord1  26446  tanord  26447  logtayl  26569  n0sind  28225  nnsind  28262  iundisj2f  32519  iundisj2fi  32720  ordtconn  33915  tgoldbachgt  34654  nexntru  36392  bj-fal  36558  bj-axd2d  36581  bj-rabtr  36918  bj-rabtrALT  36919  bj-dfid2ALT  37053  bj-finsumval0  37273  wl-impchain-mp-x  37435  wl-impchain-com-1.x  37439  wl-impchain-com-n.m  37444  wl-impchain-a1-x  37448  wl-moteq  37502  ftc1anclem5  37691  lhpexle1  40002  3lexlogpow5ineq2  42043  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  mzpcompact2lem  42739  ifpdfor  43454  ifpim1  43458  ifpnot  43459  ifpid2  43460  ifpim2  43461  uun0.1  44767  uunT1  44769  un10  44777  un01  44778  dfbi1ALTa  44929  simprimi  44930  n0abso  44966  liminfvalxr  45781  ovn02  46566  rmotru  48791  reutru  48792