Theorem tru 1376

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

Syntax hints:   → wi 4  ∀wal 1370   = wceq 1372  ⊤wtru 1373

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 1375

This theorem is referenced by:  fal  1379  dftru2  1380  mptru  1381  tbtru  1382  bitru  1384  trud  1388  truan  1389  truorfal  1425  falortru  1426  truimfal  1429  nftru  1488  euotd  4298  rabxfr  4516  reuhyp  4518  elabrex  5825  elabrexg  5826  caovcl  6100  caovass  6106  caovdi  6125  ectocl  6688  reef11  11981  mpomulcn  15009  bj-sbimeh  15670  bdtru  15730  bj-nn0suc0  15848