Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  tru GIF version

Theorem tru 1247
 Description: The truth value ⊤ is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
Assertion
Ref Expression
tru

Proof of Theorem tru
StepHypRef Expression
1 id 19 . 2 (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥)
2 df-tru 1246 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 134 1
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1241   = wceq 1243  ⊤wtru 1244 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-tru 1246 This theorem is referenced by:  fal  1250  dftru2  1251  trud  1252  tbtru  1253  bitru  1255  a1tru  1259  truan  1260  truorfal  1297  falortru  1298  truimfal  1301  nftru  1355  euotd  3991  rabxfr  4202  reuhyp  4204  elabrex  5397  caovcl  5655  caovass  5661  caovdi  5680  ectocl  6173  bj-sbimeh  9912  bdtru  9952  bj-nn0suc0  10075
 Copyright terms: Public domain W3C validator