Theorem tru 1377

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

Syntax hints:   → wi 4  ∀wal 1371   = wceq 1373  ⊤wtru 1374

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 1376

This theorem is referenced by:  fal  1380  dftru2  1381  mptru  1382  tbtru  1383  bitru  1385  trud  1389  truan  1390  truorfal  1426  falortru  1427  truimfal  1430  nftru  1490  euotd  4317  rabxfr  4535  reuhyp  4537  elabrex  5849  elabrexg  5850  caovcl  6124  caovass  6130  caovdi  6149  ectocl  6712  reef11  12125  mpomulcn  15153  bj-sbimeh  15908  bdtru  15967  bj-nn0suc0  16085