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  3203  difss2  3291  ddifstab  3295  abvor0dc  3474  ssdifeq0  3533  rabsnt  3697  unisng  3856  dfnfc2  3857  a9evsep  4155  axnul  4158  rabex2  4179  intid  4257  opm  4267  opth1  4269  opth  4270  copsex4g  4280  0nelop  4281  moop2  4284  pocl  4338  swopo  4341  limeq  4412  suceq  4437  eusvnfb  4489  onintexmid  4609  nn0eln0  4656  elvvuni  4727  coss1  4821  coss2  4822  dmxpm  4886  elrnmpt1  4917  soirri  5064  relcnvtr  5189  relssdmrn  5190  cnvpom  5212  fveqeq2  5567  fvsng  5758  isose  5868  canth  5875  riota2f  5899  acexmidlemab  5916  fvoveq1  5945  0neqopab  5967  ssoprab2  5978  caovcld  6077  caovcomd  6080  caovassd  6083  caovcand  6086  caovordid  6090  caovordd  6092  caovdid  6099  caovdird  6102  caovimo  6117  f1opw  6130  caofref  6159  caofinvl  6160  xpexgALT  6190  op1stg  6208  op2ndg  6209  releldm2  6243  elopabi  6253  dfmpo  6281  smoeq  6348  tfr1onlemaccex  6406  tfrcllemaccex  6419  rdgisucinc  6443  rdg0g  6446  oacl  6518  nna0r  6536  nnmsucr  6546  ercnv  6613  swoord1  6621  swoord2  6622  eqer  6624  ider  6625  iinerm  6666  brecop  6684  ixpssmapg  6787  elixpsn  6794  en1bg  6859  fundmeng  6866  xpsneng  6881  mapen  6907  phplem3g  6917  php5  6919  php5dom  6924  findcard2d  6952  findcard2sd  6953  undifdc  6985  xpfi  6993  elfir  7039  fi0  7041  ordiso2  7101  ctssdclemr  7178  nnnninfeq2  7195  nninfisol  7199  ctssexmid  7216  exmidaclem  7275  djuenun  7279  exmidapne  7327  cc1  7332  cc2lem  7333  mulidnq  7456  ltsonq  7465  halfnqq  7477  nqnq0pi  7505  nq02m  7532  cauappcvgprlemm  7712  cauappcvgprlemloc  7719  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem2  7727  cauappcvgpr  7729  ltposr  7830  0idsr  7834  1idsr  7835  mappsrprg  7871  ax1rid  7944  ax0id  7945  axpre-ltirr  7949  mulrid  8023  1p1times  8160  cnegexlem3  8203  pncan1  8403  npcan1  8404  kcnktkm1cn  8409  apirr  8632  recexap  8680  eqneg  8759  subrecap  8866  lediv2a  8922  nn1m1nn  9008  2txmxeqx  9122  subhalfhalf  9226  add1p1  9241  sub1m1  9242  cnm2m1cnm3  9243  xp1d2m1eqxm1d2  9244  div4p1lem1div2  9245  nn0addcl  9284  nn0mulcl  9285  zadd2cl  9455  nn0ledivnn  9842  nltpnft  9889  ngtmnft  9892  xrrebnd  9894  xnegneg  9908  xnegid  9934  xaddid1  9937  fzss1  10138  fzssp1  10142  fzshftral  10183  0elfz  10193  nn0fz0  10194  elfz0add  10195  fz0tp  10197  elfzoelz  10222  fzoval  10223  fzoss2  10248  fzossrbm1  10249  fzouzsplit  10255  elfzo1  10266  fzonn0p1  10287  fzossfzop1  10288  fzoend  10298  fzosplitsn  10309  fvinim0ffz  10317  2tnp1ge0ge0  10391  fldiv4p1lem1div2  10395  frec2uzltd  10495  frec2uzrand  10497  uzenom  10517  frecfzennn  10518  seqeq1  10542  iseqf1olemkle  10589  iseqf1olemklt  10590  iseqf1olemqk  10599  seq3f1olemstep  10606  seq3f1olemp  10607  seq3f1oleml  10608  seqf1oglem2  10612  seq3id  10617  seq3id2  10618  ser0f  10626  m1expcl2  10653  sqoddm1div8  10785  mulsubdivbinom2ap  10803  faclbnd  10833  facubnd  10837  bcpasc  10858  hashcl  10873  omgadd  10894  snopiswrd  10945  elovmpowrd  10976  reval  11014  imval  11015  crim  11023  replim  11024  rexuz3  11155  absval  11166  sqrt0  11169  resqrexlemp1rp  11171  resqrexlemfp1  11174  resqrex  11191  abs00  11229  leabs  11239  absimle  11249  cau3  11280  dfabsmax  11382  climshft  11469  fsum3  11552  fsumcnv  11602  fsumiun  11642  binom  11649  bcxmaslem1  11653  isumshft  11655  arisum  11663  arisum2  11664  trireciplem  11665  trirecip  11666  geo2sum2  11680  geo2lim  11681  prodf1f  11708  prod0  11750  fprodfac  11780  ege2le3  11836  ef4p  11859  efgt1p2  11860  efgt1p  11861  sinval  11867  cosval  11868  negdvdsb  11972  dvdsnegb  11973  dvdsssfz1  12017  dvds1  12018  3dvds  12029  even2n  12039  oddge22np1  12046  2tp1odd  12049  ltoddhalfle  12058  m1expo  12065  m1exp1  12066  flodddiv4  12101  bits0e  12113  bits0o  12114  bitsp1e  12116  bitsp1o  12117  bitsfzo  12119  gcdsupex  12124  gcdsupcl  12125  alginv  12215  algcvg  12216  algcvga  12219  algfx  12220  eucalgcvga  12226  lcmdvds  12247  pw2dvds  12334  oddpwdclemodd  12340  phimul  12394  eulerth  12401  pc2dvds  12499  pcz  12501  pcmpt  12512  pcmptdvds  12514  fldivp1  12517  oddprmdvds  12523  pockthg  12526  pockthi  12527  1arith  12536  zgz  12542  4sqlem19  12578  evenennn  12610  ennnfonelemp1  12623  ennnfonelemkh  12629  ennnfonelemnn0  12639  ssnnctlemct  12663  strslfv2  12722  strslfv  12723  basm  12739  ressvalsets  12742  ressbasid  12748  qusex  12968  xpsfeq  12988  intopsn  13010  mgmidmo  13015  ismgmid  13020  mgmlrid  13022  lidrideqd  13024  lidrididd  13025  grpinvalem  13028  grpinva  13029  gsum0g  13039  issgrp  13046  mnd1  13087  mnd1id  13088  idmhm  13101  issubm  13104  0mhm  13118  resmhm  13119  resmhm2  13120  resmhm2b  13121  dfgrp2  13159  isgrpid2  13172  grpidd2  13173  grpinvval  13175  grpressid  13193  grpsubid1  13217  dfgrp3mlem  13230  grplactfval  13233  imasgrp2  13240  mhmlem  13244  mulgfvalg  13251  mulgnnp1  13260  mulgsubcl  13266  mulgnncl  13267  mulgnn0cl  13268  mulgcl  13269  mulgnn0z  13279  mulgneg2  13286  mulgmodid  13291  submmulg  13296  issubg  13303  subgid  13305  subgex  13306  subg0  13310  subginv  13311  subgcl  13314  subgsub  13316  subgmulg  13318  issubg3  13322  isnsg  13332  isnsg3  13337  nmzsubg  13340  nmznsg  13343  eqgval  13353  idghm  13389  resghm  13390  ghmnsgima  13398  ablressid  13465  mgpvalg  13479  rngressid  13510  ringressid  13619  imasring  13620  opprvalg  13625  opprsubgg  13640  dvdsrex  13654  dvdsrtr  13657  unitinvcl  13679  unitinvinv  13680  unitlinv  13682  unitrinv  13683  issubrng  13755  subrngid  13757  issubrng2  13766  issubrg  13777  subrgid  13779  issubrg2  13797  rrgval  13818  isdomn  13825  lmodlema  13848  islmodd  13849  rmodislmod  13907  lsssn0  13926  sraval  13993  sraring  14005  sralmod  14006  rlmvalg  14010  rlmbasg  14011  rlmplusgg  14012  rlm0g  14013  rlmsubg  14014  rlmmulrg  14015  rlmscabas  14016  rlmvscag  14017  rlmtopng  14018  rlmdsg  14019  rlmvnegg  14021  lidlss  14032  lidlssbas  14033  lidlbas  14034  crngridl  14086  zringinvg  14160  mulgrhm  14165  znval  14192  znf1o  14207  psrelbasfun  14229  tsettps  14274  baspartn  14286  eltg  14288  en1top  14313  isopn3  14361  resttopon  14407  lmbr2  14450  cnptopresti  14474  cndis  14477  lmfpm  14479  lmcl  14481  lmff  14485  txswaphmeolem  14556  ispsmet  14559  psmet0  14563  xmetunirn  14594  bl2in  14639  metrest  14742  expcn  14805  cncfmptid  14833  negcncf  14841  negfcncf  14842  hovera  14883  hoverb  14884  limccl  14895  eldvap  14918  dvexp  14947  dvmptid  14952  dveflem  14962  dvef  14963  elply  14970  plypow  14980  dvply1  15001  logge0b  15126  logle1b  15128  logcxp  15133  fsumdvdsmul  15227  perfectlem2  15236  zabsle1  15240  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsdir2lem2  15270  lgsdir2lem4  15272  lgsdirnn0  15288  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  gausslemma2dlem1  15302  2lgslem1a1  15327  2lgslem1a2  15328  2lgslem1b  15330  2lgslem1c  15331  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgsoddprmlem2  15347  2lgsoddprmlem3d  15351  bj-ex  15408  bdth  15477  bj-indind  15578