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  1351  trujust  1374  tru  1376  dftru2  1380  truimtru  1428  falimfal  1431  3impexp  1456  19.26  1503  19.8a  1612  19.9ht  1663  ax6blem  1672  19.36i  1694  19.41h  1707  equsb1  1807  sbieh  1812  dveeq2or  1838  spsbim  1865  2ax17  1900  dvelimALT  2037  dvelimfv  2038  dvelimor  2045  moanmo  2130  nfcvf  2370  neqne  2383  neneq  2397  necon3i  2423  nebidc  2455  r19.27v  2632  r19.28v  2633  vtoclgft  2822  rspcime  2883  eueq2dc  2945  cdeqcv  2991  ru  2996  sbcied2  3035  sbcralt  3074  sbcrext  3075  csbiebt  3132  csbied2  3140  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  ssid  3212  difss2  3300  ddifstab  3304  abvor0dc  3483  ssdifeq0  3542  rabsnt  3707  unisng  3866  dfnfc2  3867  a9evsep  4165  axnul  4168  rabex2  4189  intid  4267  opm  4277  opth1  4279  opth  4280  copsex4g  4290  0nelop  4291  moop2  4294  pocl  4348  swopo  4351  limeq  4422  suceq  4447  eusvnfb  4499  onintexmid  4619  nn0eln0  4666  elvvuni  4737  coss1  4831  coss2  4832  dmxpm  4896  elrnmpt1  4927  soirri  5074  relcnvtr  5199  relssdmrn  5200  cnvpom  5222  fveqeq2  5579  fvsng  5770  isose  5880  canth  5887  riota2f  5911  acexmidlemab  5928  fvoveq1  5957  0neqopab  5980  ssoprab2  5991  caovcld  6090  caovcomd  6093  caovassd  6096  caovcand  6099  caovordid  6103  caovordd  6105  caovdid  6112  caovdird  6115  caovimo  6130  f1opw  6143  caofref  6173  caofinvl  6174  caofid0l  6175  caofid0r  6176  xpexgALT  6208  op1stg  6226  op2ndg  6227  releldm2  6261  elopabi  6271  dfmpo  6299  smoeq  6366  tfr1onlemaccex  6424  tfrcllemaccex  6437  rdgisucinc  6461  rdg0g  6464  oacl  6536  nna0r  6554  nnmsucr  6564  ercnv  6631  swoord1  6639  swoord2  6640  eqer  6642  ider  6643  iinerm  6684  brecop  6702  ixpssmapg  6805  elixpsn  6812  en1bg  6877  fundmeng  6884  xpsneng  6899  mapen  6925  phplem3g  6935  php5  6937  php5dom  6942  findcard2d  6970  findcard2sd  6971  undifdc  7003  xpfi  7011  elfir  7057  fi0  7059  ordiso2  7119  ctssdclemr  7196  nnnninfeq2  7213  nninfisol  7217  ctssexmid  7234  nninfinfwlpo  7264  exmidaclem  7302  djuenun  7306  exmidapne  7354  cc1  7359  cc2lem  7360  mulidnq  7484  ltsonq  7493  halfnqq  7505  nqnq0pi  7533  nq02m  7560  cauappcvgprlemm  7740  cauappcvgprlemloc  7747  cauappcvgprlemladdru  7751  cauappcvgprlemladdrl  7752  cauappcvgprlem2  7755  cauappcvgpr  7757  ltposr  7858  0idsr  7862  1idsr  7863  mappsrprg  7899  ax1rid  7972  ax0id  7973  axpre-ltirr  7977  mulrid  8051  1p1times  8188  cnegexlem3  8231  pncan1  8431  npcan1  8432  kcnktkm1cn  8437  apirr  8660  recexap  8708  eqneg  8787  subrecap  8894  lediv2a  8950  nn1m1nn  9036  2txmxeqx  9150  subhalfhalf  9254  add1p1  9269  sub1m1  9270  cnm2m1cnm3  9271  xp1d2m1eqxm1d2  9272  div4p1lem1div2  9273  nn0addcl  9312  nn0mulcl  9313  zadd2cl  9484  nn0ledivnn  9871  nltpnft  9918  ngtmnft  9921  xrrebnd  9923  xnegneg  9937  xnegid  9963  xaddid1  9966  fzss1  10167  fzssp1  10171  fzshftral  10212  0elfz  10222  nn0fz0  10223  elfz0add  10224  fz0tp  10226  elfzoelz  10251  fzoval  10252  fzoss2  10277  fzossrbm1  10278  fzouzsplit  10284  elfzo1  10295  fzonn0p1  10321  fzossfzop1  10322  fzoend  10332  fzosplitsn  10343  fvinim0ffz  10351  2tnp1ge0ge0  10425  fldiv4p1lem1div2  10429  frec2uzltd  10529  frec2uzrand  10531  uzenom  10551  frecfzennn  10552  seqeq1  10576  iseqf1olemkle  10623  iseqf1olemklt  10624  iseqf1olemqk  10633  seq3f1olemstep  10640  seq3f1olemp  10641  seq3f1oleml  10642  seqf1oglem2  10646  seq3id  10651  seq3id2  10652  ser0f  10660  m1expcl2  10687  sqoddm1div8  10819  mulsubdivbinom2ap  10837  faclbnd  10867  facubnd  10871  bcpasc  10892  hashcl  10907  omgadd  10928  snopiswrd  10979  elovmpowrd  11010  lswwrd  11015  ccatval1  11028  ccatsymb  11033  ccatass  11039  reval  11079  imval  11080  crim  11088  replim  11089  rexuz3  11220  absval  11231  sqrt0  11234  resqrexlemp1rp  11236  resqrexlemfp1  11239  resqrex  11256  abs00  11294  leabs  11304  absimle  11314  cau3  11345  dfabsmax  11447  climshft  11534  fsum3  11617  fsumcnv  11667  fsumiun  11707  binom  11714  bcxmaslem1  11718  isumshft  11720  arisum  11728  arisum2  11729  trireciplem  11730  trirecip  11731  geo2sum2  11745  geo2lim  11746  prodf1f  11773  prod0  11815  fprodfac  11845  ege2le3  11901  ef4p  11924  efgt1p2  11925  efgt1p  11926  sinval  11932  cosval  11933  negdvdsb  12037  dvdsnegb  12038  dvdsssfz1  12082  dvds1  12083  3dvds  12094  even2n  12104  oddge22np1  12111  2tp1odd  12114  ltoddhalfle  12123  m1expo  12130  m1exp1  12131  flodddiv4  12166  bits0e  12179  bits0o  12180  bitsp1e  12182  bitsp1o  12183  bitsfzo  12185  bitsinv1lem  12191  bitsinv1  12192  gcdsupex  12197  gcdsupcl  12198  alginv  12288  algcvg  12289  algcvga  12292  algfx  12293  eucalgcvga  12299  lcmdvds  12320  pw2dvds  12407  oddpwdclemodd  12413  phimul  12467  eulerth  12474  pc2dvds  12572  pcz  12574  pcmpt  12585  pcmptdvds  12587  fldivp1  12590  oddprmdvds  12596  pockthg  12599  pockthi  12600  1arith  12609  zgz  12615  4sqlem19  12651  evenennn  12683  ennnfonelemp1  12696  ennnfonelemkh  12702  ennnfonelemnn0  12712  ssnnctlemct  12736  strslfv2  12795  strslfv  12796  basm  12812  ressvalsets  12815  ressbasid  12821  pwsval  13041  qusex  13075  xpsfeq  13095  intopsn  13117  mgmidmo  13122  ismgmid  13127  mgmlrid  13129  lidrideqd  13131  lidrididd  13132  grpinvalem  13135  grpinva  13136  gsum0g  13146  issgrp  13153  imasmnd2  13202  mnd1  13205  mnd1id  13206  idmhm  13219  issubm  13222  0mhm  13236  resmhm  13237  resmhm2  13238  resmhm2b  13239  dfgrp2  13277  isgrpid2  13290  grpidd2  13291  grpinvval  13293  grpressid  13311  grpsubid1  13335  dfgrp3mlem  13348  grplactfval  13351  imasgrp2  13364  mhmlem  13368  mulgfvalg  13375  mulgnnp1  13384  mulgsubcl  13390  mulgnncl  13391  mulgnn0cl  13392  mulgcl  13393  mulgnn0z  13403  mulgneg2  13410  mulgmodid  13415  submmulg  13420  issubg  13427  subgid  13429  subgex  13430  subg0  13434  subginv  13435  subgcl  13438  subgsub  13440  subgmulg  13442  issubg3  13446  isnsg  13456  isnsg3  13461  nmzsubg  13464  nmznsg  13467  eqgval  13477  idghm  13513  resghm  13514  ghmnsgima  13522  ablressid  13589  mgpvalg  13603  rngressid  13634  ringressid  13743  imasring  13744  opprvalg  13749  opprsubgg  13764  dvdsrex  13778  dvdsrtr  13781  unitinvcl  13803  unitinvinv  13804  unitlinv  13806  unitrinv  13807  issubrng  13879  subrngid  13881  issubrng2  13890  issubrg  13901  subrgid  13903  issubrg2  13921  rrgval  13942  isdomn  13949  lmodlema  13972  islmodd  13973  rmodislmod  14031  lsssn0  14050  sraval  14117  sraring  14129  sralmod  14130  rlmvalg  14134  rlmbasg  14135  rlmplusgg  14136  rlm0g  14137  rlmsubg  14138  rlmmulrg  14139  rlmscabas  14140  rlmvscag  14141  rlmtopng  14142  rlmdsg  14143  rlmvnegg  14145  lidlss  14156  lidlssbas  14157  lidlbas  14158  crngridl  14210  zringinvg  14284  mulgrhm  14289  znval  14316  znf1o  14331  psrelbasfun  14357  mplvalcoe  14370  tsettps  14428  baspartn  14440  eltg  14442  en1top  14467  isopn3  14515  resttopon  14561  lmbr2  14604  cnptopresti  14628  cndis  14631  lmfpm  14633  lmcl  14635  lmff  14639  txswaphmeolem  14710  ispsmet  14713  psmet0  14717  xmetunirn  14748  bl2in  14793  metrest  14896  expcn  14959  cncfmptid  14987  negcncf  14995  negfcncf  14996  hovera  15037  hoverb  15038  limccl  15049  eldvap  15072  dvexp  15101  dvmptid  15106  dveflem  15116  dvef  15117  elply  15124  plypow  15134  dvply1  15155  logge0b  15280  logle1b  15282  logcxp  15287  fsumdvdsmul  15381  perfectlem2  15390  zabsle1  15394  lgsval  15399  lgsfvalg  15400  lgsval2lem  15405  lgsdir2lem2  15424  lgsdir2lem4  15426  lgsdirnn0  15442  gausslemma2dlem0i  15452  gausslemma2dlem1a  15453  gausslemma2dlem1  15456  2lgslem1a1  15481  2lgslem1a2  15482  2lgslem1b  15484  2lgslem1c  15485  2lgslem3a  15488  2lgslem3b  15489  2lgslem3c  15490  2lgslem3d  15491  2lgsoddprmlem2  15501  2lgsoddprmlem3d  15505  bj-ex  15562  bdth  15631  bj-indind  15732