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  100  biimprd  157  biimpcd  158  biimprcd  159  biid  170  bibi2i  226  imbi1  235  imbi2  236  bibi1  239  pm3.3  259  pm3.31  260  jctl  312  jctr  313  ancli  321  ancri  322  anc2li  327  anc2ri  328  anim12i  336  anim1i  338  anim1ci  339  anim2i  340  pm4.24  393  anass  399  mpdan  418  mpancom  419  pm5.32  449  anbi1  462  anbi2  463  mpan10  466  adantl3r  504  simpll  519  simplr  520  simprl  521  simprr  522  pm3.45  587  pm5.36  600  con2i  617  notnot  619  con3i  622  biijust  631  con3  632  con2  633  pm5.19  696  olc  701  orc  702  pm2.621  737  pm1.2  746  orim1i  750  orim2i  751  pm2.41  766  pm2.42  767  pm2.4  768  pm4.44  769  orim2  779  orbi1  782  pm2.38  793  pm2.74  797  pm3.2ni  803  biort  819  dcbiit  829  pm4.79dc  893  biantr  942  3anim1i  1175  3anim2i  1176  3anim3i  1177  mpd3an23  1329  trujust  1345  tru  1347  dftru2  1351  truimtru  1399  falimfal  1402  3impexp  1425  19.26  1469  19.8a  1578  19.9ht  1629  ax6blem  1638  19.36i  1660  19.41h  1673  equsb1  1773  sbieh  1778  dveeq2or  1804  spsbim  1831  2ax17  1866  dvelimALT  1998  dvelimfv  1999  dvelimor  2006  moanmo  2091  nfcvf  2331  neqne  2344  neneq  2358  necon3i  2384  nebidc  2416  r19.27v  2593  r19.28v  2594  vtoclgft  2776  rspcime  2837  eueq2dc  2899  cdeqcv  2945  ru  2950  sbcied2  2988  sbcralt  3027  sbcrext  3028  csbiebt  3084  csbied2  3092  cbvralcsf  3107  cbvrexcsf  3108  cbvreucsf  3109  cbvrabcsf  3110  ssid  3162  difss2  3250  ddifstab  3254  abvor0dc  3432  ssdifeq0  3491  rabsnt  3651  unisng  3806  dfnfc2  3807  a9evsep  4104  axnul  4107  intid  4202  opm  4212  opth1  4214  opth  4215  copsex4g  4225  0nelop  4226  moop2  4229  pocl  4281  swopo  4284  limeq  4355  suceq  4380  eusvnfb  4432  onintexmid  4550  nn0eln0  4597  elvvuni  4668  coss1  4759  coss2  4760  dmxpm  4824  elrnmpt1  4855  soirri  4998  relcnvtr  5123  relssdmrn  5124  cnvpom  5146  fveqeq2  5495  fvsng  5681  isose  5789  canth  5796  riota2f  5819  acexmidlemab  5836  fvoveq1  5865  0neqopab  5887  ssoprab2  5898  caovcld  5995  caovcomd  5998  caovassd  6001  caovcand  6004  caovordid  6008  caovordd  6010  caovdid  6017  caovdird  6020  caovimo  6035  f1opw  6045  caofref  6071  caofinvl  6072  xpexgALT  6101  op1stg  6118  op2ndg  6119  releldm2  6153  elopabi  6163  dfmpo  6191  smoeq  6258  tfr1onlemaccex  6316  tfrcllemaccex  6329  rdgisucinc  6353  rdg0g  6356  oacl  6428  nna0r  6446  nnmsucr  6456  ercnv  6522  swoord1  6530  swoord2  6531  eqer  6533  ider  6534  iinerm  6573  brecop  6591  ixpssmapg  6694  elixpsn  6701  en1bg  6766  fundmeng  6773  xpsneng  6788  mapen  6812  phplem3g  6822  php5  6824  php5dom  6829  findcard2d  6857  findcard2sd  6858  undifdc  6889  xpfi  6895  elfir  6938  fi0  6940  ordiso2  7000  ctssdclemr  7077  nnnninfeq2  7093  nninfisol  7097  ctssexmid  7114  exmidaclem  7164  djuenun  7168  cc1  7206  cc2lem  7207  mulidnq  7330  ltsonq  7339  halfnqq  7351  nqnq0pi  7379  nq02m  7406  cauappcvgprlemm  7586  cauappcvgprlemloc  7593  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem2  7601  cauappcvgpr  7603  ltposr  7704  0idsr  7708  1idsr  7709  mappsrprg  7745  ax1rid  7818  ax0id  7819  axpre-ltirr  7823  mulid1  7896  1p1times  8032  cnegexlem3  8075  pncan1  8275  npcan1  8276  kcnktkm1cn  8281  apirr  8503  recexap  8550  eqneg  8628  subrecap  8735  lediv2a  8790  nn1m1nn  8875  add1p1  9106  sub1m1  9107  cnm2m1cnm3  9108  xp1d2m1eqxm1d2  9109  div4p1lem1div2  9110  nn0addcl  9149  nn0mulcl  9150  zadd2cl  9320  nn0ledivnn  9703  nltpnft  9750  ngtmnft  9753  xrrebnd  9755  xnegneg  9769  xnegid  9795  xaddid1  9798  fzss1  9998  fzssp1  10002  fzshftral  10043  0elfz  10053  nn0fz0  10054  elfz0add  10055  fz0tp  10057  elfzoelz  10082  fzoval  10083  fzoss2  10107  fzossrbm1  10108  fzouzsplit  10114  elfzo1  10125  fzonn0p1  10146  fzossfzop1  10147  fzoend  10157  fzosplitsn  10168  fvinim0ffz  10176  2tnp1ge0ge0  10236  fldiv4p1lem1div2  10240  frec2uzltd  10338  frec2uzrand  10340  uzenom  10360  frecfzennn  10361  seqeq1  10383  iseqf1olemkle  10419  iseqf1olemklt  10420  iseqf1olemqk  10429  seq3f1olemstep  10436  seq3f1olemp  10437  seq3f1oleml  10438  seq3id  10443  seq3id2  10444  ser0f  10450  m1expcl2  10477  sqoddm1div8  10608  faclbnd  10654  facubnd  10658  bcpasc  10679  hashcl  10694  omgadd  10715  reval  10791  imval  10792  crim  10800  replim  10801  rexuz3  10932  absval  10943  sqrt0  10946  resqrexlemp1rp  10948  resqrexlemfp1  10951  resqrex  10968  abs00  11006  leabs  11016  absimle  11026  cau3  11057  dfabsmax  11159  climshft  11245  fsum3  11328  fsumcnv  11378  fsumiun  11418  binom  11425  bcxmaslem1  11429  isumshft  11431  arisum  11439  arisum2  11440  trireciplem  11441  trirecip  11442  geo2sum2  11456  geo2lim  11457  prodf1f  11484  prod0  11526  fprodfac  11556  ege2le3  11612  ef4p  11635  efgt1p2  11636  efgt1p  11637  sinval  11643  cosval  11644  negdvdsb  11747  dvdsnegb  11748  dvdsssfz1  11790  dvds1  11791  even2n  11811  oddge22np1  11818  2tp1odd  11821  ltoddhalfle  11830  m1expo  11837  m1exp1  11838  flodddiv4  11871  gcdsupex  11890  gcdsupcl  11891  alginv  11979  algcvg  11980  algcvga  11983  algfx  11984  eucalgcvga  11990  lcmdvds  12011  pw2dvds  12098  oddpwdclemodd  12104  phimul  12158  eulerth  12165  pc2dvds  12261  pcz  12263  pcmpt  12273  pcmptdvds  12275  fldivp1  12278  oddprmdvds  12284  pockthg  12287  pockthi  12288  1arith  12297  zgz  12303  evenennn  12326  ennnfonelemp1  12339  ennnfonelemkh  12345  ennnfonelemnn0  12355  ssnnctlemct  12379  strslfv2  12437  strslfv  12438  ressid  12456  intopsn  12598  mgmidmo  12603  ismgmid  12608  mgmlrid  12610  lidrideqd  12612  lidrididd  12613  grprinvlem  12616  grprinvd  12617  tsettps  12676  baspartn  12688  eltg  12692  en1top  12717  isopn3  12765  resttopon  12811  lmbr2  12854  cnptopresti  12878  cndis  12881  lmfpm  12883  lmcl  12885  lmff  12889  txswaphmeolem  12960  ispsmet  12963  psmet0  12967  xmetunirn  12998  bl2in  13043  metrest  13146  cncfmptid  13223  negcncf  13228  negfcncf  13229  limccl  13268  eldvap  13291  dvexp  13315  dveflem  13327  dvef  13328  logge0b  13451  logle1b  13453  logcxp  13458  zabsle1  13540  lgsval  13545  lgsfvalg  13546  lgsval2lem  13551  lgsdir2lem2  13570  lgsdir2lem4  13572  lgsdirnn0  13588  bj-ex  13643  bdth  13713  bj-indind  13814