HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  id Unicode version

Theorem id 25
Description: The identity inference.
Hypothesis
Ref Expression
ax-id.1 |- R:*
Assertion
Ref Expression
id |- R |= R

Proof of Theorem id
StepHypRef Expression
1 ax-id.1 . 2 |- R:*
21ax-id 24 1 |- R |= R
Colors of variables: type var term
Syntax hints:  *hb 3   |= wffMMJ2 11  wffMMJ2t 12
This theorem is referenced by:  mpdan  33  trul  37  tru  41  anasss  56  hbxfr  98  clf  105  alval  132  exval  133  euval  134  notval  135  imval  136  orval  137  anval  138  ax4g  139  pm2.21  143  dfan2  144  ecase  153  exlimdv2  156  exlimdv  157  ax4e  158  cla4ev  159  eta  166  cbvf  167  leqf  169  exlimd  171  exnal1  175  isfree  176  ac  184  exmid  186  notnot  187  ax3  192  ax9  199  ax10  200  ax11  201  axrep  207  axpow  208  axun  209
This theorem was proved from axioms:  ax-id 24
  Copyright terms: Public domain W3C validator