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  528  simprl  529  simprr  531  pm3.45  597  pm5.36  610  con2i  628  notnot  630  con3i  633  biijust  642  con3  643  con2  644  pm5.19  707  olc  712  orc  713  pm2.621  748  pm1.2  757  orim1i  761  orim2i  762  pm2.41  777  pm2.42  778  pm2.4  779  pm4.44  780  orim2  790  orbi1  793  pm2.38  804  pm2.74  808  pm3.2ni  814  biort  830  dcbiit  840  pm4.79dc  904  dcand  934  biantr  954  3anim1i  1187  3anim2i  1188  3anim3i  1189  mpd3an23  1350  trujust  1366  tru  1368  dftru2  1372  truimtru  1420  falimfal  1423  3impexp  1448  19.26  1492  19.8a  1601  19.9ht  1652  ax6blem  1661  19.36i  1683  19.41h  1696  equsb1  1796  sbieh  1801  dveeq2or  1827  spsbim  1854  2ax17  1889  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  moanmo  2119  nfcvf  2359  neqne  2372  neneq  2386  necon3i  2412  nebidc  2444  r19.27v  2621  r19.28v  2622  vtoclgft  2811  rspcime  2872  eueq2dc  2934  cdeqcv  2980  ru  2985  sbcied2  3024  sbcralt  3063  sbcrext  3064  csbiebt  3121  csbied2  3129  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  ssid  3200  difss2  3288  ddifstab  3292  abvor0dc  3471  ssdifeq0  3530  rabsnt  3694  unisng  3853  dfnfc2  3854  a9evsep  4152  axnul  4155  rabex2  4176  intid  4254  opm  4264  opth1  4266  opth  4267  copsex4g  4277  0nelop  4278  moop2  4281  pocl  4335  swopo  4338  limeq  4409  suceq  4434  eusvnfb  4486  onintexmid  4606  nn0eln0  4653  elvvuni  4724  coss1  4818  coss2  4819  dmxpm  4883  elrnmpt1  4914  soirri  5061  relcnvtr  5186  relssdmrn  5187  cnvpom  5209  fveqeq2  5564  fvsng  5755  isose  5865  canth  5872  riota2f  5896  acexmidlemab  5913  fvoveq1  5942  0neqopab  5964  ssoprab2  5975  caovcld  6074  caovcomd  6077  caovassd  6080  caovcand  6083  caovordid  6087  caovordd  6089  caovdid  6096  caovdird  6099  caovimo  6114  f1opw  6127  caofref  6156  caofinvl  6157  xpexgALT  6187  op1stg  6205  op2ndg  6206  releldm2  6240  elopabi  6250  dfmpo  6278  smoeq  6345  tfr1onlemaccex  6403  tfrcllemaccex  6416  rdgisucinc  6440  rdg0g  6443  oacl  6515  nna0r  6533  nnmsucr  6543  ercnv  6610  swoord1  6618  swoord2  6619  eqer  6621  ider  6622  iinerm  6663  brecop  6681  ixpssmapg  6784  elixpsn  6791  en1bg  6856  fundmeng  6863  xpsneng  6878  mapen  6904  phplem3g  6914  php5  6916  php5dom  6921  findcard2d  6949  findcard2sd  6950  undifdc  6982  xpfi  6988  elfir  7034  fi0  7036  ordiso2  7096  ctssdclemr  7173  nnnninfeq2  7190  nninfisol  7194  ctssexmid  7211  exmidaclem  7270  djuenun  7274  exmidapne  7322  cc1  7327  cc2lem  7328  mulidnq  7451  ltsonq  7460  halfnqq  7472  nqnq0pi  7500  nq02m  7527  cauappcvgprlemm  7707  cauappcvgprlemloc  7714  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem2  7722  cauappcvgpr  7724  ltposr  7825  0idsr  7829  1idsr  7830  mappsrprg  7866  ax1rid  7939  ax0id  7940  axpre-ltirr  7944  mulrid  8018  1p1times  8155  cnegexlem3  8198  pncan1  8398  npcan1  8399  kcnktkm1cn  8404  apirr  8626  recexap  8674  eqneg  8753  subrecap  8860  lediv2a  8916  nn1m1nn  9002  2txmxeqx  9116  subhalfhalf  9220  add1p1  9235  sub1m1  9236  cnm2m1cnm3  9237  xp1d2m1eqxm1d2  9238  div4p1lem1div2  9239  nn0addcl  9278  nn0mulcl  9279  zadd2cl  9449  nn0ledivnn  9836  nltpnft  9883  ngtmnft  9886  xrrebnd  9888  xnegneg  9902  xnegid  9928  xaddid1  9931  fzss1  10132  fzssp1  10136  fzshftral  10177  0elfz  10187  nn0fz0  10188  elfz0add  10189  fz0tp  10191  elfzoelz  10216  fzoval  10217  fzoss2  10242  fzossrbm1  10243  fzouzsplit  10249  elfzo1  10260  fzonn0p1  10281  fzossfzop1  10282  fzoend  10292  fzosplitsn  10303  fvinim0ffz  10311  2tnp1ge0ge0  10373  fldiv4p1lem1div2  10377  frec2uzltd  10477  frec2uzrand  10479  uzenom  10499  frecfzennn  10500  seqeq1  10524  iseqf1olemkle  10571  iseqf1olemklt  10572  iseqf1olemqk  10581  seq3f1olemstep  10588  seq3f1olemp  10589  seq3f1oleml  10590  seqf1oglem2  10594  seq3id  10599  seq3id2  10600  ser0f  10608  m1expcl2  10635  sqoddm1div8  10767  mulsubdivbinom2ap  10785  faclbnd  10815  facubnd  10819  bcpasc  10840  hashcl  10855  omgadd  10876  snopiswrd  10927  elovmpowrd  10958  reval  10996  imval  10997  crim  11005  replim  11006  rexuz3  11137  absval  11148  sqrt0  11151  resqrexlemp1rp  11153  resqrexlemfp1  11156  resqrex  11173  abs00  11211  leabs  11221  absimle  11231  cau3  11262  dfabsmax  11364  climshft  11450  fsum3  11533  fsumcnv  11583  fsumiun  11623  binom  11630  bcxmaslem1  11634  isumshft  11636  arisum  11644  arisum2  11645  trireciplem  11646  trirecip  11647  geo2sum2  11661  geo2lim  11662  prodf1f  11689  prod0  11731  fprodfac  11761  ege2le3  11817  ef4p  11840  efgt1p2  11841  efgt1p  11842  sinval  11848  cosval  11849  negdvdsb  11953  dvdsnegb  11954  dvdsssfz1  11997  dvds1  11998  even2n  12018  oddge22np1  12025  2tp1odd  12028  ltoddhalfle  12037  m1expo  12044  m1exp1  12045  flodddiv4  12078  gcdsupex  12097  gcdsupcl  12098  alginv  12188  algcvg  12189  algcvga  12192  algfx  12193  eucalgcvga  12199  lcmdvds  12220  pw2dvds  12307  oddpwdclemodd  12313  phimul  12367  eulerth  12374  pc2dvds  12471  pcz  12473  pcmpt  12484  pcmptdvds  12486  fldivp1  12489  oddprmdvds  12495  pockthg  12498  pockthi  12499  1arith  12508  zgz  12514  4sqlem19  12550  evenennn  12553  ennnfonelemp1  12566  ennnfonelemkh  12572  ennnfonelemnn0  12582  ssnnctlemct  12606  strslfv2  12665  strslfv  12666  basm  12682  ressvalsets  12685  ressbasid  12691  qusex  12911  xpsfeq  12931  intopsn  12953  mgmidmo  12958  ismgmid  12963  mgmlrid  12965  lidrideqd  12967  lidrididd  12968  grpinvalem  12971  grpinva  12972  gsum0g  12982  issgrp  12989  mnd1  13030  mnd1id  13031  idmhm  13044  issubm  13047  0mhm  13061  resmhm  13062  resmhm2  13063  resmhm2b  13064  dfgrp2  13102  isgrpid2  13115  grpidd2  13116  grpinvval  13118  grpressid  13136  grpsubid1  13160  dfgrp3mlem  13173  grplactfval  13176  imasgrp2  13183  mhmlem  13187  mulgfvalg  13194  mulgnnp1  13203  mulgsubcl  13209  mulgnncl  13210  mulgnn0cl  13211  mulgcl  13212  mulgnn0z  13222  mulgneg2  13229  mulgmodid  13234  submmulg  13239  issubg  13246  subgid  13248  subgex  13249  subg0  13253  subginv  13254  subgcl  13257  subgsub  13259  subgmulg  13261  issubg3  13265  isnsg  13275  isnsg3  13280  nmzsubg  13283  nmznsg  13286  eqgval  13296  idghm  13332  resghm  13333  ghmnsgima  13341  ablressid  13408  mgpvalg  13422  rngressid  13453  ringressid  13562  imasring  13563  opprvalg  13568  opprsubgg  13583  dvdsrex  13597  dvdsrtr  13600  unitinvcl  13622  unitinvinv  13623  unitlinv  13625  unitrinv  13626  issubrng  13698  subrngid  13700  issubrng2  13709  issubrg  13720  subrgid  13722  issubrg2  13740  rrgval  13761  isdomn  13768  lmodlema  13791  islmodd  13792  rmodislmod  13850  lsssn0  13869  sraval  13936  sraring  13948  sralmod  13949  rlmvalg  13953  rlmbasg  13954  rlmplusgg  13955  rlm0g  13956  rlmsubg  13957  rlmmulrg  13958  rlmscabas  13959  rlmvscag  13960  rlmtopng  13961  rlmdsg  13962  rlmvnegg  13964  lidlss  13975  lidlssbas  13976  lidlbas  13977  crngridl  14029  zringinvg  14103  mulgrhm  14108  znval  14135  znf1o  14150  psrelbasfun  14172  tsettps  14217  baspartn  14229  eltg  14231  en1top  14256  isopn3  14304  resttopon  14350  lmbr2  14393  cnptopresti  14417  cndis  14420  lmfpm  14422  lmcl  14424  lmff  14428  txswaphmeolem  14499  ispsmet  14502  psmet0  14506  xmetunirn  14537  bl2in  14582  metrest  14685  expcn  14748  cncfmptid  14776  negcncf  14784  negfcncf  14785  hovera  14826  hoverb  14827  limccl  14838  eldvap  14861  dvexp  14890  dvmptid  14895  dveflem  14905  dvef  14906  elply  14913  plypow  14923  dvply1  14943  logge0b  15066  logle1b  15068  logcxp  15073  zabsle1  15156  lgsval  15161  lgsfvalg  15162  lgsval2lem  15167  lgsdir2lem2  15186  lgsdir2lem4  15188  lgsdirnn0  15204  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  gausslemma2dlem1  15218  2lgslem1a1  15243  2lgslem1a2  15244  2lgslem1b  15246  2lgslem1c  15247  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgsoddprmlem2  15263  2lgsoddprmlem3d  15267  bj-ex  15324  bdth  15393  bj-indind  15494