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  1495  19.8a  1604  19.9ht  1655  ax6blem  1664  19.36i  1686  19.41h  1699  equsb1  1799  sbieh  1804  dveeq2or  1830  spsbim  1857  2ax17  1892  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  moanmo  2122  nfcvf  2362  neqne  2375  neneq  2389  necon3i  2415  nebidc  2447  r19.27v  2624  r19.28v  2625  vtoclgft  2814  rspcime  2875  eueq2dc  2937  cdeqcv  2983  ru  2988  sbcied2  3027  sbcralt  3066  sbcrext  3067  csbiebt  3124  csbied2  3132  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  ssid  3204  difss2  3292  ddifstab  3296  abvor0dc  3475  ssdifeq0  3534  rabsnt  3698  unisng  3857  dfnfc2  3858  a9evsep  4156  axnul  4159  rabex2  4180  intid  4258  opm  4268  opth1  4270  opth  4271  copsex4g  4281  0nelop  4282  moop2  4285  pocl  4339  swopo  4342  limeq  4413  suceq  4438  eusvnfb  4490  onintexmid  4610  nn0eln0  4657  elvvuni  4728  coss1  4822  coss2  4823  dmxpm  4887  elrnmpt1  4918  soirri  5065  relcnvtr  5190  relssdmrn  5191  cnvpom  5213  fveqeq2  5570  fvsng  5761  isose  5871  canth  5878  riota2f  5902  acexmidlemab  5919  fvoveq1  5948  0neqopab  5971  ssoprab2  5982  caovcld  6081  caovcomd  6084  caovassd  6087  caovcand  6090  caovordid  6094  caovordd  6096  caovdid  6103  caovdird  6106  caovimo  6121  f1opw  6134  caofref  6164  caofinvl  6165  caofid0l  6166  caofid0r  6167  xpexgALT  6199  op1stg  6217  op2ndg  6218  releldm2  6252  elopabi  6262  dfmpo  6290  smoeq  6357  tfr1onlemaccex  6415  tfrcllemaccex  6428  rdgisucinc  6452  rdg0g  6455  oacl  6527  nna0r  6545  nnmsucr  6555  ercnv  6622  swoord1  6630  swoord2  6631  eqer  6633  ider  6634  iinerm  6675  brecop  6693  ixpssmapg  6796  elixpsn  6803  en1bg  6868  fundmeng  6875  xpsneng  6890  mapen  6916  phplem3g  6926  php5  6928  php5dom  6933  findcard2d  6961  findcard2sd  6962  undifdc  6994  xpfi  7002  elfir  7048  fi0  7050  ordiso2  7110  ctssdclemr  7187  nnnninfeq2  7204  nninfisol  7208  ctssexmid  7225  exmidaclem  7291  djuenun  7295  exmidapne  7343  cc1  7348  cc2lem  7349  mulidnq  7473  ltsonq  7482  halfnqq  7494  nqnq0pi  7522  nq02m  7549  cauappcvgprlemm  7729  cauappcvgprlemloc  7736  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem2  7744  cauappcvgpr  7746  ltposr  7847  0idsr  7851  1idsr  7852  mappsrprg  7888  ax1rid  7961  ax0id  7962  axpre-ltirr  7966  mulrid  8040  1p1times  8177  cnegexlem3  8220  pncan1  8420  npcan1  8421  kcnktkm1cn  8426  apirr  8649  recexap  8697  eqneg  8776  subrecap  8883  lediv2a  8939  nn1m1nn  9025  2txmxeqx  9139  subhalfhalf  9243  add1p1  9258  sub1m1  9259  cnm2m1cnm3  9260  xp1d2m1eqxm1d2  9261  div4p1lem1div2  9262  nn0addcl  9301  nn0mulcl  9302  zadd2cl  9472  nn0ledivnn  9859  nltpnft  9906  ngtmnft  9909  xrrebnd  9911  xnegneg  9925  xnegid  9951  xaddid1  9954  fzss1  10155  fzssp1  10159  fzshftral  10200  0elfz  10210  nn0fz0  10211  elfz0add  10212  fz0tp  10214  elfzoelz  10239  fzoval  10240  fzoss2  10265  fzossrbm1  10266  fzouzsplit  10272  elfzo1  10283  fzonn0p1  10304  fzossfzop1  10305  fzoend  10315  fzosplitsn  10326  fvinim0ffz  10334  2tnp1ge0ge0  10408  fldiv4p1lem1div2  10412  frec2uzltd  10512  frec2uzrand  10514  uzenom  10534  frecfzennn  10535  seqeq1  10559  iseqf1olemkle  10606  iseqf1olemklt  10607  iseqf1olemqk  10616  seq3f1olemstep  10623  seq3f1olemp  10624  seq3f1oleml  10625  seqf1oglem2  10629  seq3id  10634  seq3id2  10635  ser0f  10643  m1expcl2  10670  sqoddm1div8  10802  mulsubdivbinom2ap  10820  faclbnd  10850  facubnd  10854  bcpasc  10875  hashcl  10890  omgadd  10911  snopiswrd  10962  elovmpowrd  10993  reval  11031  imval  11032  crim  11040  replim  11041  rexuz3  11172  absval  11183  sqrt0  11186  resqrexlemp1rp  11188  resqrexlemfp1  11191  resqrex  11208  abs00  11246  leabs  11256  absimle  11266  cau3  11297  dfabsmax  11399  climshft  11486  fsum3  11569  fsumcnv  11619  fsumiun  11659  binom  11666  bcxmaslem1  11670  isumshft  11672  arisum  11680  arisum2  11681  trireciplem  11682  trirecip  11683  geo2sum2  11697  geo2lim  11698  prodf1f  11725  prod0  11767  fprodfac  11797  ege2le3  11853  ef4p  11876  efgt1p2  11877  efgt1p  11878  sinval  11884  cosval  11885  negdvdsb  11989  dvdsnegb  11990  dvdsssfz1  12034  dvds1  12035  3dvds  12046  even2n  12056  oddge22np1  12063  2tp1odd  12066  ltoddhalfle  12075  m1expo  12082  m1exp1  12083  flodddiv4  12118  bits0e  12131  bits0o  12132  bitsp1e  12134  bitsp1o  12135  bitsfzo  12137  bitsinv1lem  12143  bitsinv1  12144  gcdsupex  12149  gcdsupcl  12150  alginv  12240  algcvg  12241  algcvga  12244  algfx  12245  eucalgcvga  12251  lcmdvds  12272  pw2dvds  12359  oddpwdclemodd  12365  phimul  12419  eulerth  12426  pc2dvds  12524  pcz  12526  pcmpt  12537  pcmptdvds  12539  fldivp1  12542  oddprmdvds  12548  pockthg  12551  pockthi  12552  1arith  12561  zgz  12567  4sqlem19  12603  evenennn  12635  ennnfonelemp1  12648  ennnfonelemkh  12654  ennnfonelemnn0  12664  ssnnctlemct  12688  strslfv2  12747  strslfv  12748  basm  12764  ressvalsets  12767  ressbasid  12773  pwsval  12993  qusex  13027  xpsfeq  13047  intopsn  13069  mgmidmo  13074  ismgmid  13079  mgmlrid  13081  lidrideqd  13083  lidrididd  13084  grpinvalem  13087  grpinva  13088  gsum0g  13098  issgrp  13105  imasmnd2  13154  mnd1  13157  mnd1id  13158  idmhm  13171  issubm  13174  0mhm  13188  resmhm  13189  resmhm2  13190  resmhm2b  13191  dfgrp2  13229  isgrpid2  13242  grpidd2  13243  grpinvval  13245  grpressid  13263  grpsubid1  13287  dfgrp3mlem  13300  grplactfval  13303  imasgrp2  13316  mhmlem  13320  mulgfvalg  13327  mulgnnp1  13336  mulgsubcl  13342  mulgnncl  13343  mulgnn0cl  13344  mulgcl  13345  mulgnn0z  13355  mulgneg2  13362  mulgmodid  13367  submmulg  13372  issubg  13379  subgid  13381  subgex  13382  subg0  13386  subginv  13387  subgcl  13390  subgsub  13392  subgmulg  13394  issubg3  13398  isnsg  13408  isnsg3  13413  nmzsubg  13416  nmznsg  13419  eqgval  13429  idghm  13465  resghm  13466  ghmnsgima  13474  ablressid  13541  mgpvalg  13555  rngressid  13586  ringressid  13695  imasring  13696  opprvalg  13701  opprsubgg  13716  dvdsrex  13730  dvdsrtr  13733  unitinvcl  13755  unitinvinv  13756  unitlinv  13758  unitrinv  13759  issubrng  13831  subrngid  13833  issubrng2  13842  issubrg  13853  subrgid  13855  issubrg2  13873  rrgval  13894  isdomn  13901  lmodlema  13924  islmodd  13925  rmodislmod  13983  lsssn0  14002  sraval  14069  sraring  14081  sralmod  14082  rlmvalg  14086  rlmbasg  14087  rlmplusgg  14088  rlm0g  14089  rlmsubg  14090  rlmmulrg  14091  rlmscabas  14092  rlmvscag  14093  rlmtopng  14094  rlmdsg  14095  rlmvnegg  14097  lidlss  14108  lidlssbas  14109  lidlbas  14110  crngridl  14162  zringinvg  14236  mulgrhm  14241  znval  14268  znf1o  14283  psrelbasfun  14305  tsettps  14358  baspartn  14370  eltg  14372  en1top  14397  isopn3  14445  resttopon  14491  lmbr2  14534  cnptopresti  14558  cndis  14561  lmfpm  14563  lmcl  14565  lmff  14569  txswaphmeolem  14640  ispsmet  14643  psmet0  14647  xmetunirn  14678  bl2in  14723  metrest  14826  expcn  14889  cncfmptid  14917  negcncf  14925  negfcncf  14926  hovera  14967  hoverb  14968  limccl  14979  eldvap  15002  dvexp  15031  dvmptid  15036  dveflem  15046  dvef  15047  elply  15054  plypow  15064  dvply1  15085  logge0b  15210  logle1b  15212  logcxp  15217  fsumdvdsmul  15311  perfectlem2  15320  zabsle1  15324  lgsval  15329  lgsfvalg  15330  lgsval2lem  15335  lgsdir2lem2  15354  lgsdir2lem4  15356  lgsdirnn0  15372  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  gausslemma2dlem1  15386  2lgslem1a1  15411  2lgslem1a2  15412  2lgslem1b  15414  2lgslem1c  15415  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgsoddprmlem2  15431  2lgsoddprmlem3d  15435  bj-ex  15492  bdth  15561  bj-indind  15662