Theorem id 19

Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT 20. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Assertion

Ref	Expression
id	⊢ (𝜑 → 𝜑)

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-1 5	. 2 ⊢ (𝜑 → (𝜑 → 𝜑))
2		ax-1 5	. 2 ⊢ (𝜑 → ((𝜑 → 𝜑) → 𝜑))
3	1, 2	mpd 13	1 ⊢ (𝜑 → 𝜑)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  40  pm2.43i  49  pm2.43d  50  pm2.43a  51  imim2  55  imim1i  60  imim1  76  pm2.04  82  pm2.86  100  biimprd  157  biimpcd  158  biimprcd  159  biid  170  bibi2i  226  imbi1  235  imbi2  236  bibi1  239  pm3.3  259  pm3.31  260  jctl  310  jctr  311  ancli  319  ancri  320  anc2li  325  anc2ri  326  anim12i  334  anim1i  336  anim2i  337  pm4.24  390  anass  396  mpdan  415  mpancom  416  pm5.32  446  anbi1  459  anbi2  460  mpan10  463  simpll  501  simplr  502  simprl  503  simprr  504  pm3.45  569  pm5.36  582  con2i  599  notnot  601  con3i  604  biijust  613  con3  614  con2  615  pm5.19  678  olc  683  orc  684  pm2.621  719  pm1.2  728  orim1i  732  orim2i  733  pm2.41  748  pm2.42  749  pm2.4  750  pm4.44  751  orim2  761  orbi1  764  pm2.38  775  pm2.74  779  pm3.2ni  785  dcbiit  807  pm4.79dc  869  biantr  917  3anim1i  1148  3anim2i  1149  3anim3i  1150  mpd3an23  1298  trujust  1314  tru  1316  dftru2  1320  truimtru  1368  falimfal  1371  3impexp  1394  19.26  1438  19.8a  1550  19.9ht  1601  ax6blem  1609  19.36i  1631  19.41h  1644  equsb1  1739  sbieh  1744  dveeq2or  1768  spsbim  1795  2ax17  1830  dvelimALT  1959  dvelimfv  1960  dvelimor  1967  moanmo  2050  nfcvf  2275  neqne  2288  neneq  2302  necon3i  2328  nebidc  2360  r19.27v  2531  r19.28v  2532  vtoclgft  2705  eueq2dc  2824  cdeqcv  2870  ru  2875  sbcied2  2912  sbcralt  2951  sbcrext  2952  csbiebt  3003  csbied2  3011  cbvralcsf  3026  cbvrexcsf  3027  cbvreucsf  3028  cbvrabcsf  3029  ssid  3081  difss2  3168  ddifstab  3172  abvor0dc  3350  ssdifeq0  3409  rabsnt  3562  unisng  3717  dfnfc2  3718  a9evsep  4008  axnul  4011  intid  4104  opm  4114  opth1  4116  opth  4117  copsex4g  4127  0nelop  4128  moop2  4131  pocl  4183  swopo  4186  limeq  4257  suceq  4282  eusvnfb  4333  onintexmid  4445  nn0eln0  4491  elvvuni  4561  coss1  4652  coss2  4653  dmxpm  4717  elrnmpt1  4748  soirri  4889  relcnvtr  5014  relssdmrn  5015  cnvpom  5037  fveqeq2  5382  fvsng  5568  isose  5674  riota2f  5703  acexmidlemab  5720  fvoveq1  5749  0neqopab  5768  ssoprab2  5779  caovcld  5876  caovcomd  5879  caovassd  5882  caovcand  5885  caovordid  5889  caovordd  5891  caovdid  5898  caovdird  5901  caovimo  5916  grprinvlem  5917  grprinvd  5918  f1opw  5929  caofref  5955  caofinvl  5956  xpexgALT  5983  op1stg  6000  op2ndg  6001  releldm2  6035  elopabi  6045  dfmpo  6072  smoeq  6139  tfr1onlemaccex  6197  tfrcllemaccex  6210  rdgisucinc  6234  rdg0g  6237  oacl  6308  nna0r  6326  nnmsucr  6336  ercnv  6402  swoord1  6410  swoord2  6411  eqer  6413  ider  6414  iinerm  6453  brecop  6471  ixpssmapg  6574  elixpsn  6581  en1bg  6646  fundmeng  6653  xpsneng  6667  mapen  6691  phplem3g  6701  php5  6703  php5dom  6708  findcard2d  6736  findcard2sd  6737  undifdc  6763  xpfi  6769  elfir  6811  fi0  6813  ordiso2  6870  ctssdclemr  6947  ctssexmid  6972  exmidaclem  7009  djuenun  7013  mulidnq  7139  ltsonq  7148  halfnqq  7160  nqnq0pi  7188  nq02m  7215  cauappcvgprlemm  7395  cauappcvgprlemloc  7402  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  cauappcvgprlem2  7410  cauappcvgpr  7412  ltposr  7500  0idsr  7504  1idsr  7505  ax1rid  7606  ax0id  7607  axpre-ltirr  7611  mulid1  7681  1p1times  7813  cnegexlem3  7856  pncan1  8052  npcan1  8053  kcnktkm1cn  8058  apirr  8279  recexap  8321  eqneg  8399  lediv2a  8557  nn1m1nn  8642  add1p1  8867  sub1m1  8868  cnm2m1cnm3  8869  xp1d2m1eqxm1d2  8870  div4p1lem1div2  8871  nn0addcl  8910  nn0mulcl  8911  zadd2cl  9078  nn0ledivnn  9441  nltpnft  9484  ngtmnft  9487  xrrebnd  9489  xnegneg  9503  xnegid  9529  xaddid1  9532  fzss1  9730  fzssp1  9734  fzshftral  9775  0elfz  9785  nn0fz0  9786  elfz0add  9787  fz0tp  9788  elfzoelz  9811  fzoval  9812  fzoss2  9836  fzossrbm1  9837  fzouzsplit  9843  elfzo1  9854  fzonn0p1  9875  fzossfzop1  9876  fzoend  9886  fzosplitsn  9897  fvinim0ffz  9905  2tnp1ge0ge0  9961  fldiv4p1lem1div2  9965  frec2uzltd  10063  frec2uzrand  10065  uzenom  10085  frecfzennn  10086  seqeq1  10108  iseqf1olemkle  10144  iseqf1olemklt  10145  iseqf1olemqk  10154  seq3f1olemstep  10161  seq3f1olemp  10162  seq3f1oleml  10163  seq3id  10168  seq3id2  10169  ser0f  10175  m1expcl2  10202  sqoddm1div8  10331  faclbnd  10374  facubnd  10378  bcpasc  10399  hashcl  10414  omgadd  10435  reval  10508  imval  10509  crim  10517  replim  10518  rexuz3  10648  absval  10659  sqrt0  10662  resqrexlemp1rp  10664  resqrexlemfp1  10667  resqrex  10684  abs00  10722  leabs  10732  absimle  10742  cau3  10773  dfabsmax  10875  climshft  10959  fsum3  11042  fsumcnv  11092  fsumiun  11132  binom  11139  bcxmaslem1  11143  isumshft  11145  arisum  11153  arisum2  11154  trireciplem  11155  trirecip  11156  geo2sum2  11170  geo2lim  11171  ege2le3  11222  ef4p  11245  efgt1p2  11246  efgt1p  11247  sinval  11254  cosval  11255  negdvdsb  11351  dvdsnegb  11352  dvdsssfz1  11392  dvds1  11393  even2n  11413  oddge22np1  11420  2tp1odd  11423  ltoddhalfle  11432  m1expo  11439  m1exp1  11440  flodddiv4  11473  gcdsupex  11488  gcdsupcl  11489  alginv  11568  algcvg  11569  algcvga  11572  algfx  11573  eucalgcvga  11579  lcmdvds  11600  pw2dvds  11683  oddpwdclemodd  11689  phimul  11741  evenennn  11745  ennnfonelemp1  11758  ennnfonelemkh  11764  ennnfonelemnn0  11774  strslfv2  11839  strslfv  11840  ressid  11857  tsettps  12042  baspartn  12054  eltg  12058  en1top  12083  isopn3  12131  resttopon  12177  lmbr2  12219  cnptopresti  12243  cndis  12246  lmfpm  12248  lmcl  12250  lmff  12254  ispsmet  12306  psmet0  12310  xmetunirn  12341  bl2in  12386  metrest  12489  cncfmptid  12563  negcncf  12568  negfcncf  12569  limccl  12578  eldvap  12600  bj-ex  12653  bdth  12712  bj-indind  12813