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	|- ( ph -> ph )

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 |- ( ph -> ( ph -> ph ) )
2		ax-1 6	. 2 |- ( ph -> ( ( ph -> ph ) -> ph ) )
3	1, 2	mpd 13	1 |- ( ph -> ph )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used 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  399  anass  405  mpdan  425  mpancom  426  pm5.32  457  anbi1  470  anbi2  471  mpan10  478  adantl3r  516  simpll  531  simplr  533  simprl  535  simprr  537  pm3.45  605  pm5.36  618  con2i  636  notnot  638  con3i  641  biijust  650  con3  651  con2  652  pm5.19  718  olc  723  orc  724  pm2.621  759  pm1.2  768  orim1i  772  orim2i  773  pm2.41  788  pm2.42  789  pm2.4  790  pm4.44  791  orim2  801  orbi1  804  pm2.38  815  pm2.74  819  pm3.2ni  825  biort  841  dcbiit  851  pm4.79dc  915  dcand  945  biantr  965  3anim1i  1216  3anim2i  1217  3anim3i  1218  mpd3an23  1380  trujust  1404  tru  1406  dftru2  1410  truimtru  1458  falimfal  1461  3impexp  1487  19.26  1534  19.8a  1643  19.9ht  1694  hbn  1703  19.36i  1724  19.41h  1737  equsb1  1838  sbieh  1843  dveeq2or  1869  spsbim  1896  2ax17  1931  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  moanmo  2164  nfcvf  2415  neqne  2428  neneq  2442  necon3i  2468  nebidc  2500  r19.27v  2678  r19.28v  2679  vtoclgft  2873  rspcime  2937  eueq2dc  2999  cdeqcv  3045  ru  3050  sbcied2  3089  sbcralt  3128  sbcrext  3129  csbiebt  3187  csbied2  3195  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  ssid  3268  difss2  3357  ddifstab  3361  abvor0dc  3545  ssdifeq0  3610  rabsnt  3786  unisng  3952  dfnfc2  3953  ssbr  4174  a9evsep  4255  axnul  4258  sepab  4278  rabex2  4282  intid  4364  opm  4374  opth1  4376  opth  4377  copsex4g  4387  0nelop  4388  moop2  4392  pocl  4448  swopo  4451  limeq  4522  suceq  4547  eusvnfb  4600  onintexmid  4720  nn0eln0  4767  elvvuni  4839  coss1  4935  coss2  4936  dmxpm  5002  elrnmpt1  5033  soirri  5182  relcnvtr  5307  relssdmrn  5308  cnvpom  5330  fveqeq2  5704  fsn2g  5883  funopsn  5891  fvsng  5911  isose  6027  canth  6036  riota2f  6061  riotaeqimp  6063  acexmidlemab  6079  fvoveq1  6108  0neqopab  6133  ssoprab2  6144  caovcld  6243  caovcomd  6246  caovassd  6249  caovcand  6252  caovordid  6256  caovordd  6258  caovdid  6265  caovdird  6268  caovimo  6283  f1opw  6297  caofref  6327  caofinvl  6328  caofid0l  6329  caofid0r  6330  xpexgALT  6366  op1stg  6384  op2ndg  6385  releldm2  6419  opabn1stprc  6429  elopabi  6431  dfmpo  6459  smoeq  6561  tfr1onlemaccex  6619  tfrcllemaccex  6632  rdgisucinc  6656  rdg0g  6659  oacl  6733  nna0r  6751  nnmsucr  6761  ercnv  6828  swoord1  6836  swoord2  6837  eqer  6839  ider  6840  iinerm  6881  brecop  6899  fsetdmprc0  6950  ixpssmapg  7010  elixpsn  7017  en1bg  7087  fundmeng  7095  rex2dom  7110  xpsneng  7120  mapen  7146  phplem3g  7157  php5  7159  php5dom  7164  findcard2d  7195  findcard2sd  7196  undifdc  7231  xpfi  7239  fsuppxpfi  7296  elfir  7307  fi0  7309  ordiso2  7375  ctssdclemr  7452  nnnninfeq2  7469  nninfisol  7473  ctssexmid  7490  nninfinfwlpo  7520  exmidaclem  7564  djuenun  7568  papeq2  7610  papirr  7611  exmidapne  7626  cc1  7631  cc2lem  7632  mulidnq  7756  ltsonq  7765  halfnqq  7777  nqnq0pi  7805  nq02m  7832  cauappcvgprlemm  8012  cauappcvgprlemloc  8019  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  cauappcvgpr  8029  ltposr  8130  0idsr  8134  1idsr  8135  mappsrprg  8171  ax1rid  8244  ax0id  8245  axpre-ltirr  8249  mulrid  8323  1p1times  8460  cnegexlem3  8503  pncan1  8704  npcan1  8705  kcnktkm1cn  8710  apirr  8933  recexap  8981  msq0  8997  eqneg  9062  subrecap  9169  lediv2a  9225  nn1m1nn  9322  2txmxeqx  9436  subhalfhalf  9540  add1p1  9555  sub1m1  9556  cnm2m1cnm3  9557  xp1d2m1eqxm1d2  9558  div4p1lem1div2  9559  nn0addcl  9598  nn0mulcl  9599  zadd2cl  9775  nn0ledivnn  10168  nltpnft  10216  ngtmnft  10219  xrrebnd  10221  xnegneg  10235  xnegid  10261  xaddid1  10264  fzss1  10469  fzssp1  10473  fzshftral  10515  0elfz  10525  nn0fz0  10526  elfz0add  10527  fz0tp  10529  elfzoelz  10554  fzoval  10555  fzoss2  10581  fzossrbm1  10582  fzouzsplit  10588  elfzo1  10603  fzonn0p1  10629  fzossfzop1  10630  fzoend  10640  fzosplitsn  10651  fvinim0ffz  10660  2tnp1ge0ge0  10736  fldiv4p1lem1div2  10740  frec2uzltd  10840  frec2uzrand  10842  uzenom  10862  frecfzennn  10863  seqeq1  10887  iseqf1olemkle  10934  iseqf1olemklt  10935  iseqf1olemqk  10944  seq3f1olemstep  10951  seq3f1olemp  10952  seq3f1oleml  10953  seqf1oglem2  10957  seq3id  10962  seq3id2  10963  ser0f  10971  m1expcl2  10998  resq01  11095  sqoddm1div8  11131  mulsubdivbinom2ap  11149  faclbnd  11179  facubnd  11183  bcpasc  11204  hashcl  11220  omgadd  11242  hashfibc  11283  snopiswrd  11314  elovmpowrd  11346  lswwrd  11351  ccatval1  11365  ccatsymb  11370  ccatass  11376  ccat1st1st  11409  swrdf  11427  pfxsuff1eqwrdeq  11471  ccatpfx  11473  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12  11505  swrdccatin2d  11516  reuccatpfxs1lem  11518  s3eq2  11549  reval  11614  imval  11615  crim  11623  replim  11624  sq01  11660  rexuz3  11756  absval  11767  sqrt0  11770  resqrexlemp1rp  11772  resqrexlemfp1  11775  resqrex  11792  abs00  11830  leabs  11840  absimle  11850  cau3  11881  dfabsmax  11983  climshft  12070  fsum3  12154  fsumcnv  12204  fsumiun  12244  binom  12251  bcxmaslem1  12255  isumshft  12257  arisum  12265  arisum2  12266  trireciplem  12267  trirecip  12268  geo2sum2  12282  geo2lim  12283  prodf1f  12310  prod0  12352  fprodfac  12382  ege2le3  12438  ef4p  12461  efgt1p2  12462  efgt1p  12463  sinval  12469  cosval  12470  negdvdsb  12574  dvdsnegb  12575  dvdsssfz1  12619  dvds1  12620  3dvds  12631  even2n  12641  oddge22np1  12648  2tp1odd  12651  ltoddhalfle  12660  m1expo  12667  m1exp1  12668  flodddiv4  12703  bits0e  12716  bits0o  12717  bitsp1e  12719  bitsp1o  12720  bitsfzo  12722  bitsinv1lem  12728  bitsinv1  12729  gcdsupex  12734  gcdsupcl  12735  alginv  12825  algcvg  12826  algcvga  12829  algfx  12830  eucalgcvga  12836  lcmdvds  12857  pw2dvds  12944  oddpwdclemodd  12950  phimul  13004  eulerth  13011  pc2dvds  13109  pcz  13111  pcmpt  13122  pcmptdvds  13124  fldivp1  13127  oddprmdvds  13133  pockthg  13136  pockthi  13137  1arith  13146  zgz  13152  4sqlem19  13188  ballotfilemfmpn  13234  ballotfilemfval0  13235  ballotfilemsv  13253  ballotfilemsf1o  13257  ballotfilemrval  13261  ballotfilemro  13266  ballotfilemrinv  13277  ballotfi  13282  evenennn  13284  ennnfonelemp1  13297  ennnfonelemkh  13303  ennnfonelemnn0  13313  ssnnctlemct  13337  strslfv2  13396  strslfv  13397  basm  13414  slotm  13415  ressvalsets  13418  ressbasid  13424  qusex  13646  xpsfeq  13666  intopsn  13687  mgmidmo  13692  ismgmid  13697  mgmlrid  13699  lidrideqd  13701  lidrididd  13702  grpinvalem  13705  grpinva  13706  gzsum0  13713  issgrp  13718  imasmnd2  13759  mnd1  13762  mnd1id  13763  idmhm  13776  issubm  13779  0mhm  13793  resmhm  13794  resmhm2  13795  resmhm2b  13796  dfgrp2  13832  isgrpid2  13845  grpidd2  13846  grpinvval  13848  grpressid  13866  grpsubid1  13890  dfgrp3mlem  13903  grplactfval  13906  imasgrp2  13913  mhmlem  13917  mulgfvalg  13924  mulgnnp1  13933  mulgsubcl  13939  mulgnncl  13940  mulgnn0cl  13941  mulgcl  13942  mulgnn0z  13952  mulgneg2  13959  mulgmodid  13964  submmulg  13969  issubg  13976  subgid  13978  subgex  13979  subg0  13983  subginv  13984  subgcl  13987  subgsub  13989  subgmulg  13991  issubg3  13995  isnsg  14005  isnsg3  14010  nmzsubg  14013  nmznsg  14016  eqgval  14026  idghm  14062  resghm  14063  ghmnsgima  14071  ablressid  14139  gsum0cmn  14154  pwsval  14204  mgpvalg  14220  rngressid  14253  ringressid  14368  imasring  14369  opprvalg  14374  opprsubgg  14390  dvdsrex  14405  dvdsrtr  14408  unitinvcl  14430  unitinvinv  14431  unitlinv  14433  unitrinv  14434  opprlring  14504  issubrng  14507  subrngid  14509  issubrng2  14518  issubrg  14529  subrgid  14531  issubrg2  14549  rrgval  14570  isdomn  14578  aprprop  14601  drnggrp  14613  opprdrng  14620  lmodlema  14628  islmodd  14629  rmodislmod  14688  lsssn0  14707  sraval  14774  sraring  14786  sralmod  14787  rlmvalg  14791  rlmbasg  14792  rlmplusgg  14793  rlm0g  14794  rlmsubg  14795  rlmmulrg  14796  rlmscabas  14797  rlmvscag  14798  rlmtopng  14799  rlmdsg  14800  rlmvnegg  14802  lidlss  14813  lidlssbas  14814  lidlbas  14815  crngridl  14867  zringinvg  14939  mulgrhm  14944  znval  14971  znf1o  14986  aspval  15015  asclfval  15021  psrbagfsupp  15055  psrbaglesupp  15058  psrbaglecl  15060  psrbagcon  15062  psrelbasfun  15068  mplvalcoe  15081  tsettps  15139  baspartn  15151  eltg  15153  en1top  15178  isopn3  15226  resttopon  15272  lmbr2  15315  cnptopresti  15339  cndis  15342  lmfpm  15344  lmcl  15346  lmff  15350  txswaphmeolem  15421  ispsmet  15424  psmet0  15428  xmetunirn  15459  bl2in  15504  metrest  15607  expcn  15670  cncfmptid  15698  negcncf  15706  negfcncf  15707  hovera  15748  hoverb  15749  limccl  15760  eldvap  15783  dvexp  15812  dvmptid  15817  dveflem  15827  dvef  15828  elply  15835  plypow  15845  dvply1  15866  logge0b  15991  logle1b  15993  logfac  15995  logcxp  15999  log2tlbndlog2  16082  fsumdvdsmul  16105  perfectlem2  16114  zabsle1  16118  lgsval  16123  lgsfvalg  16124  lgsval2lem  16129  lgsdir2lem2  16148  lgsdir2lem4  16150  lgsdirnn0  16166  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  gausslemma2dlem1  16180  2lgslem1a1  16205  2lgslem1a2  16206  2lgslem1b  16208  2lgslem1c  16209  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgsoddprmlem2  16225  2lgsoddprmlem3d  16229  edgfndxid  16250  uhgr0e  16323  umgrislfupgrdom  16372  ausgrusgrien  16412  egrsubgr  16504  uhgrsubgrself  16507  uhgrspanop  16523  clwwlkext2edg  16663  clwwlknccat  16664  clwwlknonmpo  16669  iseupth  16688  bj-ex  16790  bdth  16857  bj-indind  16958  exmidcon  17037  exmidpeirce  17038