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

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  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