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

Theorem tru 1263
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 1262 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 138 1
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257   = wceq 1259  wtru 1260
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-tru 1262
This theorem is referenced by:  fal  1266  dftru2  1267  trud  1268  tbtru  1269  bitru  1271  a1tru  1275  truan  1276  truorfal  1313  falortru  1314  truimfal  1317  nftru  1371  euotd  4018  rabxfr  4229  reuhyp  4231  elabrex  5424  caovcl  5682  caovass  5688  caovdi  5707  ectocl  6203  bj-sbimeh  10278  bdtru  10318  bj-nn0suc0  10441
  Copyright terms: Public domain W3C validator