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  4272  rabxfr  4488  reuhyp  4490  elabrex  5779  elabrexg  5780  caovcl  6052  caovass  6058  caovdi  6077  ectocl  6629  reef11  11742  bj-sbimeh  15002  bdtru  15062  bj-nn0suc0  15180