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 ⊢ ⊤

Syntax hints:   → wi 4  ∀wal 1400   = wceq 1402  ⊤wtru 1403

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 1405

This theorem is referenced by:  fal  1409  dftru2  1410  mptru  1411  tbtru  1412  bitru  1414  trud  1418  truan  1419  truorfal  1455  falortru  1456  truimfal  1459  nftru  1519  euotd  4390  rabxfr  4611  reuhyp  4613  elabrex  5953  elabrexg  5954  caovcl  6234  caovass  6240  caovdi  6259  ectocl  6866  reef11  12444  mpomulcn  15590  bj-sbimeh  16714  bdtru  16772  bj-nn0suc0  16890