Theorem tru 1368

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

Syntax hints:   → wi 4  ∀wal 1362   = wceq 1364  ⊤wtru 1365

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 1367

This theorem is referenced by:  fal  1371  dftru2  1372  mptru  1373  tbtru  1374  bitru  1376  trud  1380  truan  1381  truorfal  1417  falortru  1418  truimfal  1421  nftru  1477  euotd  4283  rabxfr  4501  reuhyp  4503  elabrex  5800  elabrexg  5801  caovcl  6073  caovass  6079  caovdi  6098  ectocl  6656  reef11  11842  bj-sbimeh  15264  bdtru  15324  bj-nn0suc0  15442