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

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  713  olc  718  orc  719  pm2.621  754  pm1.2  763  orim1i  767  orim2i  768  pm2.41  783  pm2.42  784  pm2.4  785  pm4.44  786  orim2  796  orbi1  799  pm2.38  810  pm2.74  814  pm3.2ni  820  biort  836  dcbiit  846  pm4.79dc  910  dcand  940  biantr  960  3anim1i  1211  3anim2i  1212  3anim3i  1213  mpd3an23  1375  trujust  1399  tru  1401  dftru2  1405  truimtru  1453  falimfal  1456  3impexp  1482  19.26  1529  19.8a  1638  19.9ht  1689  ax6blem  1698  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  2397  neqne  2410  neneq  2424  necon3i  2450  nebidc  2482  r19.27v  2660  r19.28v  2661  vtoclgft  2854  rspcime  2917  eueq2dc  2979  cdeqcv  3025  ru  3030  sbcied2  3069  sbcralt  3108  sbcrext  3109  csbiebt  3167  csbied2  3175  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  ssid  3247  difss2  3335  ddifstab  3339  abvor0dc  3518  ssdifeq0  3577  rabsnt  3746  unisng  3910  dfnfc2  3911  ssbr  4132  a9evsep  4211  axnul  4214  rabex2  4236  intid  4316  opm  4326  opth1  4328  opth  4329  copsex4g  4339  0nelop  4340  moop2  4344  pocl  4400  swopo  4403  limeq  4474  suceq  4499  eusvnfb  4551  onintexmid  4671  nn0eln0  4718  elvvuni  4790  coss1  4885  coss2  4886  dmxpm  4952  elrnmpt1  4983  soirri  5131  relcnvtr  5256  relssdmrn  5257  cnvpom  5279  fveqeq2  5648  funopsn  5829  fvsng  5849  isose  5961  canth  5968  riota2f  5993  riotaeqimp  5995  acexmidlemab  6011  fvoveq1  6040  0neqopab  6065  ssoprab2  6076  caovcld  6175  caovcomd  6178  caovassd  6181  caovcand  6184  caovordid  6188  caovordd  6190  caovdid  6197  caovdird  6200  caovimo  6215  f1opw  6229  caofref  6259  caofinvl  6260  caofid0l  6261  caofid0r  6262  xpexgALT  6294  op1stg  6312  op2ndg  6313  releldm2  6347  opabn1stprc  6357  elopabi  6359  dfmpo  6387  smoeq  6455  tfr1onlemaccex  6513  tfrcllemaccex  6526  rdgisucinc  6550  rdg0g  6553  oacl  6627  nna0r  6645  nnmsucr  6655  ercnv  6722  swoord1  6730  swoord2  6731  eqer  6733  ider  6734  iinerm  6775  brecop  6793  ixpssmapg  6896  elixpsn  6903  en1bg  6973  fundmeng  6981  rex2dom  6995  xpsneng  7005  mapen  7031  phplem3g  7041  php5  7043  php5dom  7048  findcard2d  7079  findcard2sd  7080  undifdc  7115  xpfi  7123  elfir  7171  fi0  7173  ordiso2  7233  ctssdclemr  7310  nnnninfeq2  7327  nninfisol  7331  ctssexmid  7348  nninfinfwlpo  7378  exmidaclem  7422  djuenun  7426  exmidapne  7478  cc1  7483  cc2lem  7484  mulidnq  7608  ltsonq  7617  halfnqq  7629  nqnq0pi  7657  nq02m  7684  cauappcvgprlemm  7864  cauappcvgprlemloc  7871  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem2  7879  cauappcvgpr  7881  ltposr  7982  0idsr  7986  1idsr  7987  mappsrprg  8023  ax1rid  8096  ax0id  8097  axpre-ltirr  8101  mulrid  8175  1p1times  8312  cnegexlem3  8355  pncan1  8555  npcan1  8556  kcnktkm1cn  8561  apirr  8784  recexap  8832  eqneg  8911  subrecap  9018  lediv2a  9074  nn1m1nn  9160  2txmxeqx  9274  subhalfhalf  9378  add1p1  9393  sub1m1  9394  cnm2m1cnm3  9395  xp1d2m1eqxm1d2  9396  div4p1lem1div2  9397  nn0addcl  9436  nn0mulcl  9437  zadd2cl  9608  nn0ledivnn  10001  nltpnft  10048  ngtmnft  10051  xrrebnd  10053  xnegneg  10067  xnegid  10093  xaddid1  10096  fzss1  10297  fzssp1  10301  fzshftral  10342  0elfz  10352  nn0fz0  10353  elfz0add  10354  fz0tp  10356  elfzoelz  10381  fzoval  10382  fzoss2  10408  fzossrbm1  10409  fzouzsplit  10415  elfzo1  10429  fzonn0p1  10455  fzossfzop1  10456  fzoend  10466  fzosplitsn  10477  fvinim0ffz  10486  2tnp1ge0ge0  10560  fldiv4p1lem1div2  10564  frec2uzltd  10664  frec2uzrand  10666  uzenom  10686  frecfzennn  10687  seqeq1  10711  iseqf1olemkle  10758  iseqf1olemklt  10759  iseqf1olemqk  10768  seq3f1olemstep  10775  seq3f1olemp  10776  seq3f1oleml  10777  seqf1oglem2  10781  seq3id  10786  seq3id2  10787  ser0f  10795  m1expcl2  10822  sqoddm1div8  10954  mulsubdivbinom2ap  10972  faclbnd  11002  facubnd  11006  bcpasc  11027  hashcl  11042  omgadd  11064  snopiswrd  11122  elovmpowrd  11154  lswwrd  11159  ccatval1  11173  ccatsymb  11178  ccatass  11184  ccat1st1st  11217  swrdf  11235  pfxsuff1eqwrdeq  11279  ccatpfx  11281  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12  11313  swrdccatin2d  11324  reuccatpfxs1lem  11326  s3eq2  11357  reval  11409  imval  11410  crim  11418  replim  11419  rexuz3  11550  absval  11561  sqrt0  11564  resqrexlemp1rp  11566  resqrexlemfp1  11569  resqrex  11586  abs00  11624  leabs  11634  absimle  11644  cau3  11675  dfabsmax  11777  climshft  11864  fsum3  11947  fsumcnv  11997  fsumiun  12037  binom  12044  bcxmaslem1  12048  isumshft  12050  arisum  12058  arisum2  12059  trireciplem  12060  trirecip  12061  geo2sum2  12075  geo2lim  12076  prodf1f  12103  prod0  12145  fprodfac  12175  ege2le3  12231  ef4p  12254  efgt1p2  12255  efgt1p  12256  sinval  12262  cosval  12263  negdvdsb  12367  dvdsnegb  12368  dvdsssfz1  12412  dvds1  12413  3dvds  12424  even2n  12434  oddge22np1  12441  2tp1odd  12444  ltoddhalfle  12453  m1expo  12460  m1exp1  12461  flodddiv4  12496  bits0e  12509  bits0o  12510  bitsp1e  12512  bitsp1o  12513  bitsfzo  12515  bitsinv1lem  12521  bitsinv1  12522  gcdsupex  12527  gcdsupcl  12528  alginv  12618  algcvg  12619  algcvga  12622  algfx  12623  eucalgcvga  12629  lcmdvds  12650  pw2dvds  12737  oddpwdclemodd  12743  phimul  12797  eulerth  12804  pc2dvds  12902  pcz  12904  pcmpt  12915  pcmptdvds  12917  fldivp1  12920  oddprmdvds  12926  pockthg  12929  pockthi  12930  1arith  12939  zgz  12945  4sqlem19  12981  evenennn  13013  ennnfonelemp1  13026  ennnfonelemkh  13032  ennnfonelemnn0  13042  ssnnctlemct  13066  strslfv2  13125  strslfv  13126  basm  13143  ressvalsets  13146  ressbasid  13152  pwsval  13373  qusex  13407  xpsfeq  13427  intopsn  13449  mgmidmo  13454  ismgmid  13459  mgmlrid  13461  lidrideqd  13463  lidrididd  13464  grpinvalem  13467  grpinva  13468  gsum0g  13478  issgrp  13485  imasmnd2  13534  mnd1  13537  mnd1id  13538  idmhm  13551  issubm  13554  0mhm  13568  resmhm  13569  resmhm2  13570  resmhm2b  13571  dfgrp2  13609  isgrpid2  13622  grpidd2  13623  grpinvval  13625  grpressid  13643  grpsubid1  13667  dfgrp3mlem  13680  grplactfval  13683  imasgrp2  13696  mhmlem  13700  mulgfvalg  13707  mulgnnp1  13716  mulgsubcl  13722  mulgnncl  13723  mulgnn0cl  13724  mulgcl  13725  mulgnn0z  13735  mulgneg2  13742  mulgmodid  13747  submmulg  13752  issubg  13759  subgid  13761  subgex  13762  subg0  13766  subginv  13767  subgcl  13770  subgsub  13772  subgmulg  13774  issubg3  13778  isnsg  13788  isnsg3  13793  nmzsubg  13796  nmznsg  13799  eqgval  13809  idghm  13845  resghm  13846  ghmnsgima  13854  ablressid  13921  mgpvalg  13935  rngressid  13966  ringressid  14075  imasring  14076  opprvalg  14081  opprsubgg  14096  dvdsrex  14111  dvdsrtr  14114  unitinvcl  14136  unitinvinv  14137  unitlinv  14139  unitrinv  14140  issubrng  14212  subrngid  14214  issubrng2  14223  issubrg  14234  subrgid  14236  issubrg2  14254  rrgval  14275  isdomn  14282  lmodlema  14305  islmodd  14306  rmodislmod  14364  lsssn0  14383  sraval  14450  sraring  14462  sralmod  14463  rlmvalg  14467  rlmbasg  14468  rlmplusgg  14469  rlm0g  14470  rlmsubg  14471  rlmmulrg  14472  rlmscabas  14473  rlmvscag  14474  rlmtopng  14475  rlmdsg  14476  rlmvnegg  14478  lidlss  14489  lidlssbas  14490  lidlbas  14491  crngridl  14543  zringinvg  14617  mulgrhm  14622  znval  14649  znf1o  14664  psrelbasfun  14690  mplvalcoe  14703  tsettps  14761  baspartn  14773  eltg  14775  en1top  14800  isopn3  14848  resttopon  14894  lmbr2  14937  cnptopresti  14961  cndis  14964  lmfpm  14966  lmcl  14968  lmff  14972  txswaphmeolem  15043  ispsmet  15046  psmet0  15050  xmetunirn  15081  bl2in  15126  metrest  15229  expcn  15292  cncfmptid  15320  negcncf  15328  negfcncf  15329  hovera  15370  hoverb  15371  limccl  15382  eldvap  15405  dvexp  15434  dvmptid  15439  dveflem  15449  dvef  15450  elply  15457  plypow  15467  dvply1  15488  logge0b  15613  logle1b  15615  logcxp  15620  fsumdvdsmul  15714  perfectlem2  15723  zabsle1  15727  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsdir2lem2  15757  lgsdir2lem4  15759  lgsdirnn0  15775  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  gausslemma2dlem1  15789  2lgslem1a1  15814  2lgslem1a2  15815  2lgslem1b  15817  2lgslem1c  15818  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgsoddprmlem2  15834  2lgsoddprmlem3d  15838  edgfndxid  15859  uhgr0e  15932  umgrislfupgrdom  15981  ausgrusgrien  16021  egrsubgr  16113  uhgrsubgrself  16116  uhgrspanop  16132  clwwlkext2edg  16272  clwwlknccat  16273  clwwlknonmpo  16278  iseupth  16297  bj-ex  16358  bdth  16426  bj-indind  16527  gfsum0  16682