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

Theorem tru 1336
 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 1335 . 2 (⊤ ↔ (∀𝑥 𝑥 = 𝑥 → ∀𝑥 𝑥 = 𝑥))
31, 2mpbir 145 1
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1330   = wceq 1332  ⊤wtru 1333 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116  df-tru 1335 This theorem is referenced by:  fal  1339  dftru2  1340  mptru  1341  tbtru  1342  bitru  1344  a1tru  1348  truan  1349  truorfal  1385  falortru  1386  truimfal  1389  nftru  1443  euotd  4187  rabxfr  4402  reuhyp  4404  elabrex  5671  caovcl  5937  caovass  5943  caovdi  5962  ectocl  6508  reef11  11478  bj-sbimeh  13189  bdtru  13246  bj-nn0suc0  13364
 Copyright terms: Public domain W3C validator