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. (Contributed by Mario Carneiro, 7-Oct-2014.)
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 was proved from axioms:  ax-id 24
This theorem is referenced by:  mpdan  35  trul  39  tru  44  anasss  61  hbxfr  108  clf  115  alval  142  exval  143  euval  144  notval  145  imval  146  orval  147  anval  148  ax4g  149  pm2.21  153  dfan2  154  ecase  163  exlimdv2  166  exlimdv  167  ax4e  168  cla4ev  169  eta  178  cbvf  179  leqf  181  exlimd  183  exnal1  187  isfree  188  ac  197  exmid  199  notnot  200  ax3  205  ax9  212  ax10  213  ax11  214  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator