Theorem id 25

Description: The identity inference.

Hypothesis

Ref	Expression
ax-id.1	|- R:*

Assertion

Ref	Expression
id	|- R |= R

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-id.1	. 2 |- R:*
2	1	ax-id 24	1 |- R |= R

Syntax hints:  *hb 3   |= wffMMJ2 11  wffMMJ2t 12

This theorem was proved from axioms:  ax-id 24

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