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  4295  pocl  4349  swopo  4352  limeq  4423  suceq  4448  eusvnfb  4500  onintexmid  4620  nn0eln0  4667  elvvuni  4738  coss1  4832  coss2  4833  dmxpm  4897  elrnmpt1  4928  soirri  5076  relcnvtr  5201  relssdmrn  5202  cnvpom  5224  fveqeq2  5584  funopsn  5761  fvsng  5779  isose  5889  canth  5896  riota2f  5920  acexmidlemab  5937  fvoveq1  5966  0neqopab  5989  ssoprab2  6000  caovcld  6099  caovcomd  6102  caovassd  6105  caovcand  6108  caovordid  6112  caovordd  6114  caovdid  6121  caovdird  6124  caovimo  6139  f1opw  6152  caofref  6182  caofinvl  6183  caofid0l  6184  caofid0r  6185  xpexgALT  6217  op1stg  6235  op2ndg  6236  releldm2  6270  elopabi  6280  dfmpo  6308  smoeq  6375  tfr1onlemaccex  6433  tfrcllemaccex  6446  rdgisucinc  6470  rdg0g  6473  oacl  6545  nna0r  6563  nnmsucr  6573  ercnv  6640  swoord1  6648  swoord2  6649  eqer  6651  ider  6652  iinerm  6693  brecop  6711  ixpssmapg  6814  elixpsn  6821  en1bg  6891  fundmeng  6898  rex2dom  6909  xpsneng  6916  mapen  6942  phplem3g  6952  php5  6954  php5dom  6959  findcard2d  6987  findcard2sd  6988  undifdc  7020  xpfi  7028  elfir  7074  fi0  7076  ordiso2  7136  ctssdclemr  7213  nnnninfeq2  7230  nninfisol  7234  ctssexmid  7251  nninfinfwlpo  7281  exmidaclem  7319  djuenun  7323  exmidapne  7371  cc1  7376  cc2lem  7377  mulidnq  7501  ltsonq  7510  halfnqq  7522  nqnq0pi  7550  nq02m  7577  cauappcvgprlemm  7757  cauappcvgprlemloc  7764  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem2  7772  cauappcvgpr  7774  ltposr  7875  0idsr  7879  1idsr  7880  mappsrprg  7916  ax1rid  7989  ax0id  7990  axpre-ltirr  7994  mulrid  8068  1p1times  8205  cnegexlem3  8248  pncan1  8448  npcan1  8449  kcnktkm1cn  8454  apirr  8677  recexap  8725  eqneg  8804  subrecap  8911  lediv2a  8967  nn1m1nn  9053  2txmxeqx  9167  subhalfhalf  9271  add1p1  9286  sub1m1  9287  cnm2m1cnm3  9288  xp1d2m1eqxm1d2  9289  div4p1lem1div2  9290  nn0addcl  9329  nn0mulcl  9330  zadd2cl  9501  nn0ledivnn  9888  nltpnft  9935  ngtmnft  9938  xrrebnd  9940  xnegneg  9954  xnegid  9980  xaddid1  9983  fzss1  10184  fzssp1  10188  fzshftral  10229  0elfz  10239  nn0fz0  10240  elfz0add  10241  fz0tp  10243  elfzoelz  10268  fzoval  10269  fzoss2  10294  fzossrbm1  10295  fzouzsplit  10301  elfzo1  10312  fzonn0p1  10338  fzossfzop1  10339  fzoend  10349  fzosplitsn  10360  fvinim0ffz  10368  2tnp1ge0ge0  10442  fldiv4p1lem1div2  10446  frec2uzltd  10546  frec2uzrand  10548  uzenom  10568  frecfzennn  10569  seqeq1  10593  iseqf1olemkle  10640  iseqf1olemklt  10641  iseqf1olemqk  10650  seq3f1olemstep  10657  seq3f1olemp  10658  seq3f1oleml  10659  seqf1oglem2  10663  seq3id  10668  seq3id2  10669  ser0f  10677  m1expcl2  10704  sqoddm1div8  10836  mulsubdivbinom2ap  10854  faclbnd  10884  facubnd  10888  bcpasc  10909  hashcl  10924  omgadd  10945  snopiswrd  11002  elovmpowrd  11033  lswwrd  11038  ccatval1  11051  ccatsymb  11056  ccatass  11062  reval  11102  imval  11103  crim  11111  replim  11112  rexuz3  11243  absval  11254  sqrt0  11257  resqrexlemp1rp  11259  resqrexlemfp1  11262  resqrex  11279  abs00  11317  leabs  11327  absimle  11337  cau3  11368  dfabsmax  11470  climshft  11557  fsum3  11640  fsumcnv  11690  fsumiun  11730  binom  11737  bcxmaslem1  11741  isumshft  11743  arisum  11751  arisum2  11752  trireciplem  11753  trirecip  11754  geo2sum2  11768  geo2lim  11769  prodf1f  11796  prod0  11838  fprodfac  11868  ege2le3  11924  ef4p  11947  efgt1p2  11948  efgt1p  11949  sinval  11955  cosval  11956  negdvdsb  12060  dvdsnegb  12061  dvdsssfz1  12105  dvds1  12106  3dvds  12117  even2n  12127  oddge22np1  12134  2tp1odd  12137  ltoddhalfle  12146  m1expo  12153  m1exp1  12154  flodddiv4  12189  bits0e  12202  bits0o  12203  bitsp1e  12205  bitsp1o  12206  bitsfzo  12208  bitsinv1lem  12214  bitsinv1  12215  gcdsupex  12220  gcdsupcl  12221  alginv  12311  algcvg  12312  algcvga  12315  algfx  12316  eucalgcvga  12322  lcmdvds  12343  pw2dvds  12430  oddpwdclemodd  12436  phimul  12490  eulerth  12497  pc2dvds  12595  pcz  12597  pcmpt  12608  pcmptdvds  12610  fldivp1  12613  oddprmdvds  12619  pockthg  12622  pockthi  12623  1arith  12632  zgz  12638  4sqlem19  12674  evenennn  12706  ennnfonelemp1  12719  ennnfonelemkh  12725  ennnfonelemnn0  12735  ssnnctlemct  12759  strslfv2  12818  strslfv  12819  basm  12835  ressvalsets  12838  ressbasid  12844  pwsval  13065  qusex  13099  xpsfeq  13119  intopsn  13141  mgmidmo  13146  ismgmid  13151  mgmlrid  13153  lidrideqd  13155  lidrididd  13156  grpinvalem  13159  grpinva  13160  gsum0g  13170  issgrp  13177  imasmnd2  13226  mnd1  13229  mnd1id  13230  idmhm  13243  issubm  13246  0mhm  13260  resmhm  13261  resmhm2  13262  resmhm2b  13263  dfgrp2  13301  isgrpid2  13314  grpidd2  13315  grpinvval  13317  grpressid  13335  grpsubid1  13359  dfgrp3mlem  13372  grplactfval  13375  imasgrp2  13388  mhmlem  13392  mulgfvalg  13399  mulgnnp1  13408  mulgsubcl  13414  mulgnncl  13415  mulgnn0cl  13416  mulgcl  13417  mulgnn0z  13427  mulgneg2  13434  mulgmodid  13439  submmulg  13444  issubg  13451  subgid  13453  subgex  13454  subg0  13458  subginv  13459  subgcl  13462  subgsub  13464  subgmulg  13466  issubg3  13470  isnsg  13480  isnsg3  13485  nmzsubg  13488  nmznsg  13491  eqgval  13501  idghm  13537  resghm  13538  ghmnsgima  13546  ablressid  13613  mgpvalg  13627  rngressid  13658  ringressid  13767  imasring  13768  opprvalg  13773  opprsubgg  13788  dvdsrex  13802  dvdsrtr  13805  unitinvcl  13827  unitinvinv  13828  unitlinv  13830  unitrinv  13831  issubrng  13903  subrngid  13905  issubrng2  13914  issubrg  13925  subrgid  13927  issubrg2  13945  rrgval  13966  isdomn  13973  lmodlema  13996  islmodd  13997  rmodislmod  14055  lsssn0  14074  sraval  14141  sraring  14153  sralmod  14154  rlmvalg  14158  rlmbasg  14159  rlmplusgg  14160  rlm0g  14161  rlmsubg  14162  rlmmulrg  14163  rlmscabas  14164  rlmvscag  14165  rlmtopng  14166  rlmdsg  14167  rlmvnegg  14169  lidlss  14180  lidlssbas  14181  lidlbas  14182  crngridl  14234  zringinvg  14308  mulgrhm  14313  znval  14340  znf1o  14355  psrelbasfun  14381  mplvalcoe  14394  tsettps  14452  baspartn  14464  eltg  14466  en1top  14491  isopn3  14539  resttopon  14585  lmbr2  14628  cnptopresti  14652  cndis  14655  lmfpm  14657  lmcl  14659  lmff  14663  txswaphmeolem  14734  ispsmet  14737  psmet0  14741  xmetunirn  14772  bl2in  14817  metrest  14920  expcn  14983  cncfmptid  15011  negcncf  15019  negfcncf  15020  hovera  15061  hoverb  15062  limccl  15073  eldvap  15096  dvexp  15125  dvmptid  15130  dveflem  15140  dvef  15141  elply  15148  plypow  15158  dvply1  15179  logge0b  15304  logle1b  15306  logcxp  15311  fsumdvdsmul  15405  perfectlem2  15414  zabsle1  15418  lgsval  15423  lgsfvalg  15424  lgsval2lem  15429  lgsdir2lem2  15448  lgsdir2lem4  15450  lgsdirnn0  15466  gausslemma2dlem0i  15476  gausslemma2dlem1a  15477  gausslemma2dlem1  15480  2lgslem1a1  15505  2lgslem1a2  15506  2lgslem1b  15508  2lgslem1c  15509  2lgslem3a  15512  2lgslem3b  15513  2lgslem3c  15514  2lgslem3d  15515  2lgsoddprmlem2  15525  2lgsoddprmlem3d  15529  edgfndxid  15550  bj-ex  15631  bdth  15700  bj-indind  15801