Theorem tru 1406

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400   = wceq 1402  ⊤wtru 1403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-tru 1405

This theorem is used by:  fal  1409  dftru2  1410  mptru  1411  tbtru  1412  bitru  1414  trud  1418  truan  1419  truorfal  1455  falortru  1456  truimfal  1459  nftru  1519  euotd  4395  rabxfr  4616  reuhyp  4618  elabrex  5963  elabrexg  5964  caovcl  6244  caovass  6250  caovdi  6269  ectocl  6876  reef11  12466  mpomulcn  15667  bj-sbimeh  16800  bdtru  16858  bj-nn0suc0  16976