Theorem tru 1357

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

Syntax hints:   → wi 4  ∀wal 1351   = wceq 1353  ⊤wtru 1354

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 1356

This theorem is referenced by:  fal  1360  dftru2  1361  mptru  1362  tbtru  1363  bitru  1365  a1tru  1369  truan  1370  truorfal  1406  falortru  1407  truimfal  1410  nftru  1466  euotd  4255  rabxfr  4471  reuhyp  4473  elabrex  5759  caovcl  6029  caovass  6035  caovdi  6054  ectocl  6602  reef11  11707  bj-sbimeh  14527  bdtru  14587  bj-nn0suc0  14705