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

Theorem tru 1357
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 1356 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 146 1
Colors of variables: wff set class
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  4250  rabxfr  4466  reuhyp  4468  elabrex  5752  caovcl  6022  caovass  6028  caovdi  6047  ectocl  6595  reef11  11678  bj-sbimeh  14146  bdtru  14206  bj-nn0suc0  14324
  Copyright terms: Public domain W3C validator