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  4397  rabxfr  4618  reuhyp  4620  elabrex  5966  elabrexg  5967  caovcl  6247  caovass  6253  caovdi  6272  ectocl  6880  reef11  12491  mpomulcn  15792  bj-sbimeh  17005  bdtru  17063  bj-nn0suc0  17181