Theorem tru 1399

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

Syntax hints:   → wi 4  ∀wal 1393   = wceq 1395  ⊤wtru 1396

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 1398

This theorem is referenced by:  fal  1402  dftru2  1403  mptru  1404  tbtru  1405  bitru  1407  trud  1411  truan  1412  truorfal  1448  falortru  1449  truimfal  1452  nftru  1512  euotd  4341  rabxfr  4561  reuhyp  4563  elabrex  5887  elabrexg  5888  caovcl  6166  caovass  6172  caovdi  6191  ectocl  6757  reef11  12225  mpomulcn  15255  bj-sbimeh  16191  bdtru  16250  bj-nn0suc0  16368