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  529  simprl  531  simprr  533  pm3.45  601  pm5.36  614  con2i  632  notnot  634  con3i  637  biijust  646  con3  647  con2  648  pm5.19  714  olc  719  orc  720  pm2.621  755  pm1.2  764  orim1i  768  orim2i  769  pm2.41  784  pm2.42  785  pm2.4  786  pm4.44  787  orim2  797  orbi1  800  pm2.38  811  pm2.74  815  pm3.2ni  821  biort  837  dcbiit  847  pm4.79dc  911  dcand  941  biantr  961  3anim1i  1212  3anim2i  1213  3anim3i  1214  mpd3an23  1376  trujust  1400  tru  1402  dftru2  1406  truimtru  1454  falimfal  1457  3impexp  1483  19.26  1530  19.8a  1639  19.9ht  1690  hbn  1699  19.36i  1720  19.41h  1733  equsb1  1834  sbieh  1839  dveeq2or  1865  spsbim  1892  2ax17  1927  dvelimALT  2064  dvelimfv  2065  dvelimor  2072  moanmo  2158  nfcvf  2407  neqne  2420  neneq  2434  necon3i  2460  nebidc  2492  r19.27v  2670  r19.28v  2671  vtoclgft  2865  rspcime  2928  eueq2dc  2990  cdeqcv  3036  ru  3041  sbcied2  3080  sbcralt  3119  sbcrext  3120  csbiebt  3178  csbied2  3186  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  ssid  3258  difss2  3347  ddifstab  3351  abvor0dc  3532  ssdifeq0  3592  rabsnt  3766  unisng  3931  dfnfc2  3932  ssbr  4153  a9evsep  4232  axnul  4235  rabex2  4258  intid  4340  opm  4350  opth1  4352  opth  4353  copsex4g  4363  0nelop  4364  moop2  4368  pocl  4424  swopo  4427  limeq  4498  suceq  4523  eusvnfb  4575  onintexmid  4695  nn0eln0  4742  elvvuni  4814  coss1  4910  coss2  4911  dmxpm  4977  elrnmpt1  5008  soirri  5157  relcnvtr  5282  relssdmrn  5283  cnvpom  5305  fveqeq2  5679  fsn2g  5852  funopsn  5860  fvsng  5880  isose  5994  canth  6001  riota2f  6026  riotaeqimp  6028  acexmidlemab  6044  fvoveq1  6073  0neqopab  6098  ssoprab2  6109  caovcld  6208  caovcomd  6211  caovassd  6214  caovcand  6217  caovordid  6221  caovordd  6223  caovdid  6230  caovdird  6233  caovimo  6248  f1opw  6262  caofref  6291  caofinvl  6292  caofid0l  6293  caofid0r  6294  xpexgALT  6326  op1stg  6344  op2ndg  6345  releldm2  6379  opabn1stprc  6389  elopabi  6391  dfmpo  6419  smoeq  6521  tfr1onlemaccex  6579  tfrcllemaccex  6592  rdgisucinc  6616  rdg0g  6619  oacl  6693  nna0r  6711  nnmsucr  6721  ercnv  6788  swoord1  6796  swoord2  6797  eqer  6799  ider  6800  iinerm  6841  brecop  6859  ixpssmapg  6963  elixpsn  6970  en1bg  7040  fundmeng  7048  rex2dom  7063  xpsneng  7073  mapen  7099  phplem3g  7110  php5  7112  php5dom  7117  findcard2d  7148  findcard2sd  7149  undifdc  7184  xpfi  7192  fsuppxpfi  7249  elfir  7260  fi0  7262  ordiso2  7326  ctssdclemr  7403  nnnninfeq2  7420  nninfisol  7424  ctssexmid  7441  nninfinfwlpo  7471  exmidaclem  7515  djuenun  7519  papirr  7560  exmidapne  7574  cc1  7579  cc2lem  7580  mulidnq  7704  ltsonq  7713  halfnqq  7725  nqnq0pi  7753  nq02m  7780  cauappcvgprlemm  7960  cauappcvgprlemloc  7967  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  cauappcvgprlem2  7975  cauappcvgpr  7977  ltposr  8078  0idsr  8082  1idsr  8083  mappsrprg  8119  ax1rid  8192  ax0id  8193  axpre-ltirr  8197  mulrid  8271  1p1times  8407  cnegexlem3  8450  pncan1  8650  npcan1  8651  kcnktkm1cn  8656  apirr  8879  recexap  8927  eqneg  9006  subrecap  9113  lediv2a  9169  nn1m1nn  9255  2txmxeqx  9369  subhalfhalf  9473  add1p1  9488  sub1m1  9489  cnm2m1cnm3  9490  xp1d2m1eqxm1d2  9491  div4p1lem1div2  9492  nn0addcl  9531  nn0mulcl  9532  zadd2cl  9707  nn0ledivnn  10100  nltpnft  10147  ngtmnft  10150  xrrebnd  10152  xnegneg  10166  xnegid  10192  xaddid1  10195  fzss1  10397  fzssp1  10401  fzshftral  10442  0elfz  10452  nn0fz0  10453  elfz0add  10454  fz0tp  10456  elfzoelz  10481  fzoval  10482  fzoss2  10508  fzossrbm1  10509  fzouzsplit  10515  elfzo1  10530  fzonn0p1  10556  fzossfzop1  10557  fzoend  10567  fzosplitsn  10578  fvinim0ffz  10587  2tnp1ge0ge0  10661  fldiv4p1lem1div2  10665  frec2uzltd  10765  frec2uzrand  10767  uzenom  10787  frecfzennn  10788  seqeq1  10812  iseqf1olemkle  10859  iseqf1olemklt  10860  iseqf1olemqk  10869  seq3f1olemstep  10876  seq3f1olemp  10877  seq3f1oleml  10878  seqf1oglem2  10882  seq3id  10887  seq3id2  10888  ser0f  10896  m1expcl2  10923  sqoddm1div8  11055  mulsubdivbinom2ap  11073  faclbnd  11103  facubnd  11107  bcpasc  11128  hashcl  11144  omgadd  11166  hashfibc  11207  snopiswrd  11234  elovmpowrd  11266  lswwrd  11271  ccatval1  11285  ccatsymb  11290  ccatass  11296  ccat1st1st  11329  swrdf  11347  pfxsuff1eqwrdeq  11391  ccatpfx  11393  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12  11425  swrdccatin2d  11436  reuccatpfxs1lem  11438  s3eq2  11469  reval  11534  imval  11535  crim  11543  replim  11544  rexuz3  11675  absval  11686  sqrt0  11689  resqrexlemp1rp  11691  resqrexlemfp1  11694  resqrex  11711  abs00  11749  leabs  11759  absimle  11769  cau3  11800  dfabsmax  11902  climshft  11989  fsum3  12073  fsumcnv  12123  fsumiun  12163  binom  12170  bcxmaslem1  12174  isumshft  12176  arisum  12184  arisum2  12185  trireciplem  12186  trirecip  12187  geo2sum2  12201  geo2lim  12202  prodf1f  12229  prod0  12271  fprodfac  12301  ege2le3  12357  ef4p  12380  efgt1p2  12381  efgt1p  12382  sinval  12388  cosval  12389  negdvdsb  12493  dvdsnegb  12494  dvdsssfz1  12538  dvds1  12539  3dvds  12550  even2n  12560  oddge22np1  12567  2tp1odd  12570  ltoddhalfle  12579  m1expo  12586  m1exp1  12587  flodddiv4  12622  bits0e  12635  bits0o  12636  bitsp1e  12638  bitsp1o  12639  bitsfzo  12641  bitsinv1lem  12647  bitsinv1  12648  gcdsupex  12653  gcdsupcl  12654  alginv  12744  algcvg  12745  algcvga  12748  algfx  12749  eucalgcvga  12755  lcmdvds  12776  pw2dvds  12863  oddpwdclemodd  12869  phimul  12923  eulerth  12930  pc2dvds  13028  pcz  13030  pcmpt  13041  pcmptdvds  13043  fldivp1  13046  oddprmdvds  13052  pockthg  13055  pockthi  13056  1arith  13065  zgz  13071  4sqlem19  13107  evenennn  13144  ennnfonelemp1  13157  ennnfonelemkh  13163  ennnfonelemnn0  13173  ssnnctlemct  13197  strslfv2  13256  strslfv  13257  basm  13274  ressvalsets  13277  ressbasid  13283  pwsval  13504  qusex  13538  xpsfeq  13558  intopsn  13580  mgmidmo  13585  ismgmid  13590  mgmlrid  13592  lidrideqd  13594  lidrididd  13595  grpinvalem  13598  grpinva  13599  gsum0g  13609  issgrp  13616  imasmnd2  13665  mnd1  13668  mnd1id  13669  idmhm  13682  issubm  13685  0mhm  13699  resmhm  13700  resmhm2  13701  resmhm2b  13702  dfgrp2  13740  isgrpid2  13753  grpidd2  13754  grpinvval  13756  grpressid  13774  grpsubid1  13798  dfgrp3mlem  13811  grplactfval  13814  imasgrp2  13827  mhmlem  13831  mulgfvalg  13838  mulgnnp1  13847  mulgsubcl  13853  mulgnncl  13854  mulgnn0cl  13855  mulgcl  13856  mulgnn0z  13866  mulgneg2  13873  mulgmodid  13878  submmulg  13883  issubg  13890  subgid  13892  subgex  13893  subg0  13897  subginv  13898  subgcl  13901  subgsub  13903  subgmulg  13905  issubg3  13909  isnsg  13919  isnsg3  13924  nmzsubg  13927  nmznsg  13930  eqgval  13940  idghm  13976  resghm  13977  ghmnsgima  13985  ablressid  14052  mgpvalg  14067  rngressid  14098  ringressid  14207  imasring  14208  opprvalg  14213  opprsubgg  14228  dvdsrex  14243  dvdsrtr  14246  unitinvcl  14268  unitinvinv  14269  unitlinv  14271  unitrinv  14272  issubrng  14344  subrngid  14346  issubrng2  14355  issubrg  14366  subrgid  14368  issubrg2  14386  rrgval  14407  isdomn  14415  lmodlema  14440  islmodd  14441  rmodislmod  14499  lsssn0  14518  sraval  14585  sraring  14597  sralmod  14598  rlmvalg  14602  rlmbasg  14603  rlmplusgg  14604  rlm0g  14605  rlmsubg  14606  rlmmulrg  14607  rlmscabas  14608  rlmvscag  14609  rlmtopng  14610  rlmdsg  14611  rlmvnegg  14613  lidlss  14624  lidlssbas  14625  lidlbas  14626  crngridl  14678  zringinvg  14752  mulgrhm  14757  znval  14784  znf1o  14799  psrbagfsupp  14819  psrbaglesupp  14822  psrbaglecl  14824  psrbagcon  14826  psrelbasfun  14832  mplvalcoe  14845  tsettps  14903  baspartn  14915  eltg  14917  en1top  14942  isopn3  14990  resttopon  15036  lmbr2  15079  cnptopresti  15103  cndis  15106  lmfpm  15108  lmcl  15110  lmff  15114  txswaphmeolem  15185  ispsmet  15188  psmet0  15192  xmetunirn  15223  bl2in  15268  metrest  15371  expcn  15434  cncfmptid  15462  negcncf  15470  negfcncf  15471  hovera  15512  hoverb  15513  limccl  15524  eldvap  15547  dvexp  15576  dvmptid  15581  dveflem  15591  dvef  15592  elply  15599  plypow  15609  dvply1  15630  logge0b  15755  logle1b  15757  logcxp  15762  fsumdvdsmul  15859  perfectlem2  15868  zabsle1  15872  lgsval  15877  lgsfvalg  15878  lgsval2lem  15883  lgsdir2lem2  15902  lgsdir2lem4  15904  lgsdirnn0  15920  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  gausslemma2dlem1  15934  2lgslem1a1  15959  2lgslem1a2  15960  2lgslem1b  15962  2lgslem1c  15963  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgsoddprmlem2  15979  2lgsoddprmlem3d  15983  edgfndxid  16004  uhgr0e  16077  umgrislfupgrdom  16126  ausgrusgrien  16166  egrsubgr  16258  uhgrsubgrself  16261  uhgrspanop  16277  clwwlkext2edg  16417  clwwlknccat  16418  clwwlknonmpo  16423  iseupth  16442  bj-ex  16534  bdth  16601  bj-indind  16702  exmidcon  16780  exmidpeirce  16781  gfsum0  16864