Theorem tru 1402

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 19	. 2 ⊢ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2		df-tru 1401	. 2 ⊢ (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
3	1, 2	mpbir 146	1 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1396   = wceq 1398  ⊤wtru 1399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-tru 1401

This theorem is referenced by:  fal  1405  dftru2  1406  mptru  1407  tbtru  1408  bitru  1410  trud  1414  truan  1415  truorfal  1451  falortru  1452  truimfal  1455  nftru  1515  euotd  4353  rabxfr  4573  reuhyp  4575  elabrex  5908  elabrexg  5909  caovcl  6187  caovass  6193  caovdi  6212  ectocl  6814  reef11  12340  mpomulcn  15377  bj-sbimeh  16490  bdtru  16548  bj-nn0suc0  16666