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 6	. 2 |- ( ph -> ( ph -> ph ) )
2		ax-1 6	. 2 |- ( ph -> ( ( ph -> ph ) -> ph ) )
3	1, 2	mpd 13	1 |- ( ph -> ph )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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  101  biimprd  158  biimpcd  159  biimprcd  160  biid  171  bibi2i  227  imbi1  236  imbi2  237  bibi1  240  pm3.3  261  pm3.31  262  jctl  314  jctr  315  ancli  323  ancri  324  anc2li  329  anc2ri  330  anim12i  338  anim1i  340  anim1ci  341  anim2i  342  pm4.24  395  anass  401  mpdan  421  mpancom  422  pm5.32  453  anbi1  466  anbi2  467  mpan10  474  adantl3r  512  simpll  527  simplr  529  simprl  531  simprr  533  pm3.45  601  pm5.36  614  con2i  632  notnot  634  con3i  637  biijust  646  con3  647  con2  648  pm5.19  714  olc  719  orc  720  pm2.621  755  pm1.2  764  orim1i  768  orim2i  769  pm2.41  784  pm2.42  785  pm2.4  786  pm4.44  787  orim2  797  orbi1  800  pm2.38  811  pm2.74  815  pm3.2ni  821  biort  837  dcbiit  847  pm4.79dc  911  dcand  941  biantr  961  3anim1i  1212  3anim2i  1213  3anim3i  1214  mpd3an23  1376  trujust  1400  tru  1402  dftru2  1406  truimtru  1454  falimfal  1457  3impexp  1483  19.26  1530  19.8a  1639  19.9ht  1690  hbn  1699  19.36i  1720  19.41h  1733  equsb1  1833  sbieh  1838  dveeq2or  1864  spsbim  1891  2ax17  1926  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  moanmo  2157  nfcvf  2398  neqne  2411  neneq  2425  necon3i  2451  nebidc  2483  r19.27v  2661  r19.28v  2662  vtoclgft  2855  rspcime  2918  eueq2dc  2980  cdeqcv  3026  ru  3031  sbcied2  3070  sbcralt  3109  sbcrext  3110  csbiebt  3168  csbied2  3176  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  ssid  3248  difss2  3337  ddifstab  3341  abvor0dc  3520  ssdifeq0  3579  rabsnt  3750  unisng  3915  dfnfc2  3916  ssbr  4137  a9evsep  4216  axnul  4219  rabex2  4241  intid  4322  opm  4332  opth1  4334  opth  4335  copsex4g  4345  0nelop  4346  moop2  4350  pocl  4406  swopo  4409  limeq  4480  suceq  4505  eusvnfb  4557  onintexmid  4677  nn0eln0  4724  elvvuni  4796  coss1  4891  coss2  4892  dmxpm  4958  elrnmpt1  4989  soirri  5138  relcnvtr  5263  relssdmrn  5264  cnvpom  5286  fveqeq2  5657  fsn2g  5830  funopsn  5838  fvsng  5858  isose  5972  canth  5979  riota2f  6004  riotaeqimp  6006  acexmidlemab  6022  fvoveq1  6051  0neqopab  6076  ssoprab2  6087  caovcld  6186  caovcomd  6189  caovassd  6192  caovcand  6195  caovordid  6199  caovordd  6201  caovdid  6208  caovdird  6211  caovimo  6226  f1opw  6240  caofref  6269  caofinvl  6270  caofid0l  6271  caofid0r  6272  xpexgALT  6304  op1stg  6322  op2ndg  6323  releldm2  6357  opabn1stprc  6367  elopabi  6369  dfmpo  6397  smoeq  6499  tfr1onlemaccex  6557  tfrcllemaccex  6570  rdgisucinc  6594  rdg0g  6597  oacl  6671  nna0r  6689  nnmsucr  6699  ercnv  6766  swoord1  6774  swoord2  6775  eqer  6777  ider  6778  iinerm  6819  brecop  6837  ixpssmapg  6940  elixpsn  6947  en1bg  7017  fundmeng  7025  rex2dom  7039  xpsneng  7049  mapen  7075  phplem3g  7085  php5  7087  php5dom  7092  findcard2d  7123  findcard2sd  7124  undifdc  7159  xpfi  7167  fsuppxpfi  7221  elfir  7232  fi0  7234  ordiso2  7294  ctssdclemr  7371  nnnninfeq2  7388  nninfisol  7392  ctssexmid  7409  nninfinfwlpo  7439  exmidaclem  7483  djuenun  7487  exmidapne  7539  cc1  7544  cc2lem  7545  mulidnq  7669  ltsonq  7678  halfnqq  7690  nqnq0pi  7718  nq02m  7745  cauappcvgprlemm  7925  cauappcvgprlemloc  7932  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  cauappcvgprlem2  7940  cauappcvgpr  7942  ltposr  8043  0idsr  8047  1idsr  8048  mappsrprg  8084  ax1rid  8157  ax0id  8158  axpre-ltirr  8162  mulrid  8236  1p1times  8372  cnegexlem3  8415  pncan1  8615  npcan1  8616  kcnktkm1cn  8621  apirr  8844  recexap  8892  eqneg  8971  subrecap  9078  lediv2a  9134  nn1m1nn  9220  2txmxeqx  9334  subhalfhalf  9438  add1p1  9453  sub1m1  9454  cnm2m1cnm3  9455  xp1d2m1eqxm1d2  9456  div4p1lem1div2  9457  nn0addcl  9496  nn0mulcl  9497  zadd2cl  9670  nn0ledivnn  10063  nltpnft  10110  ngtmnft  10113  xrrebnd  10115  xnegneg  10129  xnegid  10155  xaddid1  10158  fzss1  10360  fzssp1  10364  fzshftral  10405  0elfz  10415  nn0fz0  10416  elfz0add  10417  fz0tp  10419  elfzoelz  10444  fzoval  10445  fzoss2  10471  fzossrbm1  10472  fzouzsplit  10478  elfzo1  10493  fzonn0p1  10519  fzossfzop1  10520  fzoend  10530  fzosplitsn  10541  fvinim0ffz  10550  2tnp1ge0ge0  10624  fldiv4p1lem1div2  10628  frec2uzltd  10728  frec2uzrand  10730  uzenom  10750  frecfzennn  10751  seqeq1  10775  iseqf1olemkle  10822  iseqf1olemklt  10823  iseqf1olemqk  10832  seq3f1olemstep  10839  seq3f1olemp  10840  seq3f1oleml  10841  seqf1oglem2  10845  seq3id  10850  seq3id2  10851  ser0f  10859  m1expcl2  10886  sqoddm1div8  11018  mulsubdivbinom2ap  11036  faclbnd  11066  facubnd  11070  bcpasc  11091  hashcl  11106  omgadd  11128  snopiswrd  11189  elovmpowrd  11221  lswwrd  11226  ccatval1  11240  ccatsymb  11245  ccatass  11251  ccat1st1st  11284  swrdf  11302  pfxsuff1eqwrdeq  11346  ccatpfx  11348  swrdccatin2  11376  pfxccatin12lem2  11378  pfxccatin12  11380  swrdccatin2d  11391  reuccatpfxs1lem  11393  s3eq2  11424  reval  11489  imval  11490  crim  11498  replim  11499  rexuz3  11630  absval  11641  sqrt0  11644  resqrexlemp1rp  11646  resqrexlemfp1  11649  resqrex  11666  abs00  11704  leabs  11714  absimle  11724  cau3  11755  dfabsmax  11857  climshft  11944  fsum3  12028  fsumcnv  12078  fsumiun  12118  binom  12125  bcxmaslem1  12129  isumshft  12131  arisum  12139  arisum2  12140  trireciplem  12141  trirecip  12142  geo2sum2  12156  geo2lim  12157  prodf1f  12184  prod0  12226  fprodfac  12256  ege2le3  12312  ef4p  12335  efgt1p2  12336  efgt1p  12337  sinval  12343  cosval  12344  negdvdsb  12448  dvdsnegb  12449  dvdsssfz1  12493  dvds1  12494  3dvds  12505  even2n  12515  oddge22np1  12522  2tp1odd  12525  ltoddhalfle  12534  m1expo  12541  m1exp1  12542  flodddiv4  12577  bits0e  12590  bits0o  12591  bitsp1e  12593  bitsp1o  12594  bitsfzo  12596  bitsinv1lem  12602  bitsinv1  12603  gcdsupex  12608  gcdsupcl  12609  alginv  12699  algcvg  12700  algcvga  12703  algfx  12704  eucalgcvga  12710  lcmdvds  12731  pw2dvds  12818  oddpwdclemodd  12824  phimul  12878  eulerth  12885  pc2dvds  12983  pcz  12985  pcmpt  12996  pcmptdvds  12998  fldivp1  13001  oddprmdvds  13007  pockthg  13010  pockthi  13011  1arith  13020  zgz  13026  4sqlem19  13062  evenennn  13094  ennnfonelemp1  13107  ennnfonelemkh  13113  ennnfonelemnn0  13123  ssnnctlemct  13147  strslfv2  13206  strslfv  13207  basm  13224  ressvalsets  13227  ressbasid  13233  pwsval  13454  qusex  13488  xpsfeq  13508  intopsn  13530  mgmidmo  13535  ismgmid  13540  mgmlrid  13542  lidrideqd  13544  lidrididd  13545  grpinvalem  13548  grpinva  13549  gsum0g  13559  issgrp  13566  imasmnd2  13615  mnd1  13618  mnd1id  13619  idmhm  13632  issubm  13635  0mhm  13649  resmhm  13650  resmhm2  13651  resmhm2b  13652  dfgrp2  13690  isgrpid2  13703  grpidd2  13704  grpinvval  13706  grpressid  13724  grpsubid1  13748  dfgrp3mlem  13761  grplactfval  13764  imasgrp2  13777  mhmlem  13781  mulgfvalg  13788  mulgnnp1  13797  mulgsubcl  13803  mulgnncl  13804  mulgnn0cl  13805  mulgcl  13806  mulgnn0z  13816  mulgneg2  13823  mulgmodid  13828  submmulg  13833  issubg  13840  subgid  13842  subgex  13843  subg0  13847  subginv  13848  subgcl  13851  subgsub  13853  subgmulg  13855  issubg3  13859  isnsg  13869  isnsg3  13874  nmzsubg  13877  nmznsg  13880  eqgval  13890  idghm  13926  resghm  13927  ghmnsgima  13935  ablressid  14002  mgpvalg  14017  rngressid  14048  ringressid  14157  imasring  14158  opprvalg  14163  opprsubgg  14178  dvdsrex  14193  dvdsrtr  14196  unitinvcl  14218  unitinvinv  14219  unitlinv  14221  unitrinv  14222  issubrng  14294  subrngid  14296  issubrng2  14305  issubrg  14316  subrgid  14318  issubrg2  14336  rrgval  14357  isdomn  14365  lmodlema  14388  islmodd  14389  rmodislmod  14447  lsssn0  14466  sraval  14533  sraring  14545  sralmod  14546  rlmvalg  14550  rlmbasg  14551  rlmplusgg  14552  rlm0g  14553  rlmsubg  14554  rlmmulrg  14555  rlmscabas  14556  rlmvscag  14557  rlmtopng  14558  rlmdsg  14559  rlmvnegg  14561  lidlss  14572  lidlssbas  14573  lidlbas  14574  crngridl  14626  zringinvg  14700  mulgrhm  14705  znval  14732  znf1o  14747  psrbaglesupp  14769  psrbaglecl  14771  psrbagcon  14772  psrelbasfun  14778  mplvalcoe  14791  tsettps  14849  baspartn  14861  eltg  14863  en1top  14888  isopn3  14936  resttopon  14982  lmbr2  15025  cnptopresti  15049  cndis  15052  lmfpm  15054  lmcl  15056  lmff  15060  txswaphmeolem  15131  ispsmet  15134  psmet0  15138  xmetunirn  15169  bl2in  15214  metrest  15317  expcn  15380  cncfmptid  15408  negcncf  15416  negfcncf  15417  hovera  15458  hoverb  15459  limccl  15470  eldvap  15493  dvexp  15522  dvmptid  15527  dveflem  15537  dvef  15538  elply  15545  plypow  15555  dvply1  15576  logge0b  15701  logle1b  15703  logcxp  15708  fsumdvdsmul  15805  perfectlem2  15814  zabsle1  15818  lgsval  15823  lgsfvalg  15824  lgsval2lem  15829  lgsdir2lem2  15848  lgsdir2lem4  15850  lgsdirnn0  15866  gausslemma2dlem0i  15876  gausslemma2dlem1a  15877  gausslemma2dlem1  15880  2lgslem1a1  15905  2lgslem1a2  15906  2lgslem1b  15908  2lgslem1c  15909  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgsoddprmlem2  15925  2lgsoddprmlem3d  15929  edgfndxid  15950  uhgr0e  16023  umgrislfupgrdom  16072  ausgrusgrien  16112  egrsubgr  16204  uhgrsubgrself  16207  uhgrspanop  16223  clwwlkext2edg  16363  clwwlknccat  16364  clwwlknonmpo  16369  iseupth  16388  bj-ex  16480  bdth  16547  bj-indind  16648  exmidcon  16728  exmidpeirce  16729  gfsum0  16811