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  599  pm5.36  612  con2i  630  notnot  632  con3i  635  biijust  644  con3  645  con2  646  pm5.19  711  olc  716  orc  717  pm2.621  752  pm1.2  761  orim1i  765  orim2i  766  pm2.41  781  pm2.42  782  pm2.4  783  pm4.44  784  orim2  794  orbi1  797  pm2.38  808  pm2.74  812  pm3.2ni  818  biort  834  dcbiit  844  pm4.79dc  908  dcand  938  biantr  958  3anim1i  1209  3anim2i  1210  3anim3i  1211  mpd3an23  1373  trujust  1397  tru  1399  dftru2  1403  truimtru  1451  falimfal  1454  3impexp  1480  19.26  1527  19.8a  1636  19.9ht  1687  ax6blem  1696  19.36i  1718  19.41h  1731  equsb1  1831  sbieh  1836  dveeq2or  1862  spsbim  1889  2ax17  1924  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  moanmo  2155  nfcvf  2395  neqne  2408  neneq  2422  necon3i  2448  nebidc  2480  r19.27v  2658  r19.28v  2659  vtoclgft  2852  rspcime  2915  eueq2dc  2977  cdeqcv  3023  ru  3028  sbcied2  3067  sbcralt  3106  sbcrext  3107  csbiebt  3165  csbied2  3173  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  ssid  3245  difss2  3333  ddifstab  3337  abvor0dc  3516  ssdifeq0  3575  rabsnt  3744  unisng  3908  dfnfc2  3909  ssbr  4130  a9evsep  4209  axnul  4212  rabex2  4234  intid  4314  opm  4324  opth1  4326  opth  4327  copsex4g  4337  0nelop  4338  moop2  4342  pocl  4398  swopo  4401  limeq  4472  suceq  4497  eusvnfb  4549  onintexmid  4669  nn0eln0  4716  elvvuni  4788  coss1  4883  coss2  4884  dmxpm  4950  elrnmpt1  4981  soirri  5129  relcnvtr  5254  relssdmrn  5255  cnvpom  5277  fveqeq2  5644  funopsn  5825  fvsng  5845  isose  5957  canth  5964  riota2f  5989  riotaeqimp  5991  acexmidlemab  6007  fvoveq1  6036  0neqopab  6061  ssoprab2  6072  caovcld  6171  caovcomd  6174  caovassd  6177  caovcand  6180  caovordid  6184  caovordd  6186  caovdid  6193  caovdird  6196  caovimo  6211  f1opw  6225  caofref  6255  caofinvl  6256  caofid0l  6257  caofid0r  6258  xpexgALT  6290  op1stg  6308  op2ndg  6309  releldm2  6343  opabn1stprc  6353  elopabi  6355  dfmpo  6383  smoeq  6451  tfr1onlemaccex  6509  tfrcllemaccex  6522  rdgisucinc  6546  rdg0g  6549  oacl  6623  nna0r  6641  nnmsucr  6651  ercnv  6718  swoord1  6726  swoord2  6727  eqer  6729  ider  6730  iinerm  6771  brecop  6789  ixpssmapg  6892  elixpsn  6899  en1bg  6969  fundmeng  6977  rex2dom  6991  xpsneng  7001  mapen  7027  phplem3g  7037  php5  7039  php5dom  7044  findcard2d  7073  findcard2sd  7074  undifdc  7109  xpfi  7117  elfir  7163  fi0  7165  ordiso2  7225  ctssdclemr  7302  nnnninfeq2  7319  nninfisol  7323  ctssexmid  7340  nninfinfwlpo  7370  exmidaclem  7413  djuenun  7417  exmidapne  7469  cc1  7474  cc2lem  7475  mulidnq  7599  ltsonq  7608  halfnqq  7620  nqnq0pi  7648  nq02m  7675  cauappcvgprlemm  7855  cauappcvgprlemloc  7862  cauappcvgprlemladdru  7866  cauappcvgprlemladdrl  7867  cauappcvgprlem2  7870  cauappcvgpr  7872  ltposr  7973  0idsr  7977  1idsr  7978  mappsrprg  8014  ax1rid  8087  ax0id  8088  axpre-ltirr  8092  mulrid  8166  1p1times  8303  cnegexlem3  8346  pncan1  8546  npcan1  8547  kcnktkm1cn  8552  apirr  8775  recexap  8823  eqneg  8902  subrecap  9009  lediv2a  9065  nn1m1nn  9151  2txmxeqx  9265  subhalfhalf  9369  add1p1  9384  sub1m1  9385  cnm2m1cnm3  9386  xp1d2m1eqxm1d2  9387  div4p1lem1div2  9388  nn0addcl  9427  nn0mulcl  9428  zadd2cl  9599  nn0ledivnn  9992  nltpnft  10039  ngtmnft  10042  xrrebnd  10044  xnegneg  10058  xnegid  10084  xaddid1  10087  fzss1  10288  fzssp1  10292  fzshftral  10333  0elfz  10343  nn0fz0  10344  elfz0add  10345  fz0tp  10347  elfzoelz  10372  fzoval  10373  fzoss2  10399  fzossrbm1  10400  fzouzsplit  10406  elfzo1  10420  fzonn0p1  10446  fzossfzop1  10447  fzoend  10457  fzosplitsn  10468  fvinim0ffz  10477  2tnp1ge0ge0  10551  fldiv4p1lem1div2  10555  frec2uzltd  10655  frec2uzrand  10657  uzenom  10677  frecfzennn  10678  seqeq1  10702  iseqf1olemkle  10749  iseqf1olemklt  10750  iseqf1olemqk  10759  seq3f1olemstep  10766  seq3f1olemp  10767  seq3f1oleml  10768  seqf1oglem2  10772  seq3id  10777  seq3id2  10778  ser0f  10786  m1expcl2  10813  sqoddm1div8  10945  mulsubdivbinom2ap  10963  faclbnd  10993  facubnd  10997  bcpasc  11018  hashcl  11033  omgadd  11055  snopiswrd  11113  elovmpowrd  11145  lswwrd  11150  ccatval1  11164  ccatsymb  11169  ccatass  11175  ccat1st1st  11208  swrdf  11226  pfxsuff1eqwrdeq  11270  ccatpfx  11272  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12  11304  swrdccatin2d  11315  reuccatpfxs1lem  11317  s3eq2  11348  reval  11400  imval  11401  crim  11409  replim  11410  rexuz3  11541  absval  11552  sqrt0  11555  resqrexlemp1rp  11557  resqrexlemfp1  11560  resqrex  11577  abs00  11615  leabs  11625  absimle  11635  cau3  11666  dfabsmax  11768  climshft  11855  fsum3  11938  fsumcnv  11988  fsumiun  12028  binom  12035  bcxmaslem1  12039  isumshft  12041  arisum  12049  arisum2  12050  trireciplem  12051  trirecip  12052  geo2sum2  12066  geo2lim  12067  prodf1f  12094  prod0  12136  fprodfac  12166  ege2le3  12222  ef4p  12245  efgt1p2  12246  efgt1p  12247  sinval  12253  cosval  12254  negdvdsb  12358  dvdsnegb  12359  dvdsssfz1  12403  dvds1  12404  3dvds  12415  even2n  12425  oddge22np1  12432  2tp1odd  12435  ltoddhalfle  12444  m1expo  12451  m1exp1  12452  flodddiv4  12487  bits0e  12500  bits0o  12501  bitsp1e  12503  bitsp1o  12504  bitsfzo  12506  bitsinv1lem  12512  bitsinv1  12513  gcdsupex  12518  gcdsupcl  12519  alginv  12609  algcvg  12610  algcvga  12613  algfx  12614  eucalgcvga  12620  lcmdvds  12641  pw2dvds  12728  oddpwdclemodd  12734  phimul  12788  eulerth  12795  pc2dvds  12893  pcz  12895  pcmpt  12906  pcmptdvds  12908  fldivp1  12911  oddprmdvds  12917  pockthg  12920  pockthi  12921  1arith  12930  zgz  12936  4sqlem19  12972  evenennn  13004  ennnfonelemp1  13017  ennnfonelemkh  13023  ennnfonelemnn0  13033  ssnnctlemct  13057  strslfv2  13116  strslfv  13117  basm  13134  ressvalsets  13137  ressbasid  13143  pwsval  13364  qusex  13398  xpsfeq  13418  intopsn  13440  mgmidmo  13445  ismgmid  13450  mgmlrid  13452  lidrideqd  13454  lidrididd  13455  grpinvalem  13458  grpinva  13459  gsum0g  13469  issgrp  13476  imasmnd2  13525  mnd1  13528  mnd1id  13529  idmhm  13542  issubm  13545  0mhm  13559  resmhm  13560  resmhm2  13561  resmhm2b  13562  dfgrp2  13600  isgrpid2  13613  grpidd2  13614  grpinvval  13616  grpressid  13634  grpsubid1  13658  dfgrp3mlem  13671  grplactfval  13674  imasgrp2  13687  mhmlem  13691  mulgfvalg  13698  mulgnnp1  13707  mulgsubcl  13713  mulgnncl  13714  mulgnn0cl  13715  mulgcl  13716  mulgnn0z  13726  mulgneg2  13733  mulgmodid  13738  submmulg  13743  issubg  13750  subgid  13752  subgex  13753  subg0  13757  subginv  13758  subgcl  13761  subgsub  13763  subgmulg  13765  issubg3  13769  isnsg  13779  isnsg3  13784  nmzsubg  13787  nmznsg  13790  eqgval  13800  idghm  13836  resghm  13837  ghmnsgima  13845  ablressid  13912  mgpvalg  13926  rngressid  13957  ringressid  14066  imasring  14067  opprvalg  14072  opprsubgg  14087  dvdsrex  14102  dvdsrtr  14105  unitinvcl  14127  unitinvinv  14128  unitlinv  14130  unitrinv  14131  issubrng  14203  subrngid  14205  issubrng2  14214  issubrg  14225  subrgid  14227  issubrg2  14245  rrgval  14266  isdomn  14273  lmodlema  14296  islmodd  14297  rmodislmod  14355  lsssn0  14374  sraval  14441  sraring  14453  sralmod  14454  rlmvalg  14458  rlmbasg  14459  rlmplusgg  14460  rlm0g  14461  rlmsubg  14462  rlmmulrg  14463  rlmscabas  14464  rlmvscag  14465  rlmtopng  14466  rlmdsg  14467  rlmvnegg  14469  lidlss  14480  lidlssbas  14481  lidlbas  14482  crngridl  14534  zringinvg  14608  mulgrhm  14613  znval  14640  znf1o  14655  psrelbasfun  14681  mplvalcoe  14694  tsettps  14752  baspartn  14764  eltg  14766  en1top  14791  isopn3  14839  resttopon  14885  lmbr2  14928  cnptopresti  14952  cndis  14955  lmfpm  14957  lmcl  14959  lmff  14963  txswaphmeolem  15034  ispsmet  15037  psmet0  15041  xmetunirn  15072  bl2in  15117  metrest  15220  expcn  15283  cncfmptid  15311  negcncf  15319  negfcncf  15320  hovera  15361  hoverb  15362  limccl  15373  eldvap  15396  dvexp  15425  dvmptid  15430  dveflem  15440  dvef  15441  elply  15448  plypow  15458  dvply1  15479  logge0b  15604  logle1b  15606  logcxp  15611  fsumdvdsmul  15705  perfectlem2  15714  zabsle1  15718  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsdir2lem2  15748  lgsdir2lem4  15750  lgsdirnn0  15766  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  gausslemma2dlem1  15780  2lgslem1a1  15805  2lgslem1a2  15806  2lgslem1b  15808  2lgslem1c  15809  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgsoddprmlem2  15825  2lgsoddprmlem3d  15829  edgfndxid  15850  uhgr0e  15923  umgrislfupgrdom  15970  ausgrusgrien  16010  clwwlkext2edg  16217  clwwlknccat  16218  clwwlknonmpo  16223  iseupth  16242  bj-ex  16294  bdth  16362  bj-indind  16463