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	|- ( ph -> ph )

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-1 5	. 2 |- ( ph -> ( ph -> ph ) )
2		ax-1 5	. 2 |- ( ph -> ( ( ph -> ph ) -> ph ) )
3	1, 2	mpd 13	1 |- ( ph -> ph )

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  258  pm3.31  259  jctl  308  jctr  309  ancli  317  ancri  318  anc2li  323  anc2ri  324  anim12i  332  anim1i  334  anim2i  335  pm4.24  388  anass  394  mpdan  413  mpancom  414  pm5.32  442  anbi1  455  anbi2  456  mpan10  459  simpll  497  simplr  498  simprl  499  simprr  500  pm3.45  565  pm5.36  578  con2i  593  notnot  595  con3i  598  biijust  606  con3  607  con2  608  notbii  630  pm5.19  658  olc  668  orc  669  pm2.621  702  pm1.2  709  orim1i  713  orim2i  714  pm2.41  729  pm2.42  730  pm2.4  731  pm4.44  732  orim2  739  orbi1  742  pm2.38  753  pm2.74  757  pm3.2ni  763  pm4.79dc  848  biantr  899  3anim1i  1130  3anim2i  1131  3anim3i  1132  mpd3an23  1276  trujust  1292  tru  1294  dftru2  1298  truimtru  1346  falimfal  1349  3impexp  1372  19.26  1416  19.8a  1528  19.9ht  1578  ax6blem  1586  19.36i  1608  19.41h  1621  equsb1  1716  sbieh  1721  dveeq2or  1745  spsbim  1772  2ax17  1807  dvelimALT  1935  dvelimfv  1936  dvelimor  1943  moanmo  2026  nfcvf  2251  neqne  2264  neneq  2278  necon3i  2304  nebidc  2336  vtoclgft  2670  eueq2dc  2789  cdeqcv  2835  ru  2840  sbcied2  2877  sbcralt  2916  sbcrext  2917  csbiebt  2968  csbied2  2976  cbvralcsf  2991  cbvrexcsf  2992  cbvreucsf  2993  cbvrabcsf  2994  ssid  3045  difss2  3129  ddifstab  3133  abvor0dc  3310  ssdifeq0  3369  ifbi  3415  rabsnt  3521  unisng  3676  dfnfc2  3677  a9evsep  3967  axnul  3970  intid  4060  opm  4070  opth1  4072  opth  4073  copsex4g  4083  0nelop  4084  moop2  4087  pocl  4139  swopo  4142  limeq  4213  suceq  4238  eusvnfb  4289  onintexmid  4401  nn0eln0  4446  elvvuni  4515  coss1  4604  coss2  4605  dmxpm  4669  elrnmpt1  4699  soirri  4839  relcnvtr  4963  relssdmrn  4964  cnvpom  4986  fveqeq2  5327  fvsng  5507  isose  5614  riota2f  5643  acexmidlemab  5660  fvoveq1  5689  0neqopab  5708  ssoprab2  5719  caovcld  5812  caovcomd  5815  caovassd  5818  caovcand  5821  caovordid  5825  caovordd  5827  caovdid  5834  caovdird  5837  caovimo  5852  grprinvlem  5853  grprinvd  5854  f1opw  5865  caofref  5890  caofinvl  5891  xpexgALT  5918  op1stg  5935  op2ndg  5936  releldm2  5969  elopabi  5979  dfmpt2  6002  smoeq  6069  tfr1onlemaccex  6127  tfrcllemaccex  6140  rdgisucinc  6164  rdg0g  6167  oacl  6235  nna0r  6253  nnmsucr  6263  ercnv  6327  swoord1  6335  swoord2  6336  eqer  6338  ider  6339  iinerm  6378  brecop  6396  ixpssmapg  6499  elixpsn  6506  en1bg  6571  fundmeng  6578  xpsneng  6592  mapen  6616  phplem3g  6626  php5  6628  php5dom  6633  findcard2d  6661  findcard2sd  6662  undifdc  6688  xpfi  6694  ordiso2  6782  mulidnq  7002  ltsonq  7011  halfnqq  7023  nqnq0pi  7051  nq02m  7078  cauappcvgprlemm  7258  cauappcvgprlemloc  7265  cauappcvgprlemladdru  7269  cauappcvgprlemladdrl  7270  cauappcvgprlem2  7273  cauappcvgpr  7275  ltposr  7363  0idsr  7367  1idsr  7368  ax1rid  7466  ax0id  7467  axpre-ltirr  7471  mulid1  7539  1p1times  7670  cnegexlem3  7713  pncan1  7909  npcan1  7910  kcnktkm1cn  7915  apirr  8136  recexap  8176  eqneg  8253  lediv2a  8410  nn1m1nn  8494  add1p1  8719  sub1m1  8720  cnm2m1cnm3  8721  xp1d2m1eqxm1d2  8722  div4p1lem1div2  8723  nn0addcl  8762  nn0mulcl  8763  zadd2cl  8929  nn0ledivnn  9292  nltpnft  9333  ngtmnft  9334  xrrebnd  9335  xnegneg  9349  fzss1  9531  fzssp1  9535  fzshftral  9576  0elfz  9586  nn0fz0  9587  elfz0add  9588  fz0tp  9589  elfzoelz  9612  fzoval  9613  fzoss2  9637  fzossrbm1  9638  fzouzsplit  9644  elfzo1  9655  fzonn0p1  9676  fzossfzop1  9677  fzoend  9687  fzosplitsn  9698  fvinim0ffz  9706  2tnp1ge0ge0  9762  fldiv4p1lem1div2  9766  frec2uzltd  9864  frec2uzrand  9866  uzenom  9886  frecfzennn  9887  iseqeq1  9912  iseqf1olemkle  9967  iseqf1olemklt  9968  iseqf1olemqk  9977  seq3f1olemstep  9984  seq3f1olemp  9985  seq3f1oleml  9986  iseqid  9993  seq3id2  9994  iseqid2  9995  iser0f  10002  ser0f  10004  m1expcl2  10031  sqoddm1div8  10160  faclbnd  10203  facubnd  10207  bcpasc  10228  hashcl  10243  omgadd  10264  reval  10337  imval  10338  crim  10346  replim  10347  rexuz3  10477  absval  10488  sqrt0  10491  resqrexlemp1rp  10493  resqrexlemfp1  10496  resqrex  10513  leabs  10561  absimle  10571  cau3  10602  dfabsmax  10704  climshft  10746  fisum  10832  fsumcnv  10885  fsumiun  10925  binom  10932  bcxmaslem1  10936  isumshft  10938  arisum  10946  arisum2  10947  trireciplem  10948  trirecip  10949  geo2sum2  10963  geo2lim  10964  ege2le3  11015  ef4p  11038  efgt1p2  11039  efgt1p  11040  sinval  11047  cosval  11048  negdvdsb  11144  dvdsnegb  11145  dvdsssfz1  11185  dvds1  11186  even2n  11206  oddge22np1  11213  2tp1odd  11216  ltoddhalfle  11225  m1expo  11232  m1exp1  11233  flodddiv4  11266  gcdsupex  11281  gcdsupcl  11282  alginv  11361  algcvg  11362  algcvga  11365  algfx  11366  eucalgcvga  11372  lcmdvds  11393  pw2dvds  11476  oddpwdclemodd  11482  phimul  11534  evenennn  11538  strslfv2  11591  strslfv  11592  ressid  11609  tsettps  11790  baspartn  11802  eltg  11806  en1top  11831  isopn3  11879  bj-ex  11929  bdth  11988  bj-dcbi  12085  bj-indind  12093