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 )

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  708  olc  713  orc  714  pm2.621  749  pm1.2  758  orim1i  762  orim2i  763  pm2.41  778  pm2.42  779  pm2.4  780  pm4.44  781  orim2  791  orbi1  794  pm2.38  805  pm2.74  809  pm3.2ni  815  biort  831  dcbiit  841  pm4.79dc  905  dcand  935  biantr  955  3anim1i  1188  3anim2i  1189  3anim3i  1190  mpd3an23  1352  trujust  1375  tru  1377  dftru2  1381  truimtru  1429  falimfal  1432  3impexp  1457  19.26  1504  19.8a  1613  19.9ht  1664  ax6blem  1673  19.36i  1695  19.41h  1708  equsb1  1808  sbieh  1813  dveeq2or  1839  spsbim  1866  2ax17  1901  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  moanmo  2131  nfcvf  2371  neqne  2384  neneq  2398  necon3i  2424  nebidc  2456  r19.27v  2633  r19.28v  2634  vtoclgft  2823  rspcime  2884  eueq2dc  2946  cdeqcv  2992  ru  2997  sbcied2  3036  sbcralt  3075  sbcrext  3076  csbiebt  3133  csbied2  3141  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  ssid  3213  difss2  3301  ddifstab  3305  abvor0dc  3484  ssdifeq0  3543  rabsnt  3708  unisng  3867  dfnfc2  3868  a9evsep  4166  axnul  4169  rabex2  4190  intid  4268  opm  4278  opth1  4280  opth  4281  copsex4g  4291  0nelop  4292  moop2  4296  pocl  4350  swopo  4353  limeq  4424  suceq  4449  eusvnfb  4501  onintexmid  4621  nn0eln0  4668  elvvuni  4739  coss1  4833  coss2  4834  dmxpm  4898  elrnmpt1  4929  soirri  5077  relcnvtr  5202  relssdmrn  5203  cnvpom  5225  fveqeq2  5585  funopsn  5762  fvsng  5780  isose  5890  canth  5897  riota2f  5921  acexmidlemab  5938  fvoveq1  5967  0neqopab  5990  ssoprab2  6001  caovcld  6100  caovcomd  6103  caovassd  6106  caovcand  6109  caovordid  6113  caovordd  6115  caovdid  6122  caovdird  6125  caovimo  6140  f1opw  6153  caofref  6183  caofinvl  6184  caofid0l  6185  caofid0r  6186  xpexgALT  6218  op1stg  6236  op2ndg  6237  releldm2  6271  elopabi  6281  dfmpo  6309  smoeq  6376  tfr1onlemaccex  6434  tfrcllemaccex  6447  rdgisucinc  6471  rdg0g  6474  oacl  6546  nna0r  6564  nnmsucr  6574  ercnv  6641  swoord1  6649  swoord2  6650  eqer  6652  ider  6653  iinerm  6694  brecop  6712  ixpssmapg  6815  elixpsn  6822  en1bg  6892  fundmeng  6899  rex2dom  6910  xpsneng  6917  mapen  6943  phplem3g  6953  php5  6955  php5dom  6960  findcard2d  6988  findcard2sd  6989  undifdc  7021  xpfi  7029  elfir  7075  fi0  7077  ordiso2  7137  ctssdclemr  7214  nnnninfeq2  7231  nninfisol  7235  ctssexmid  7252  nninfinfwlpo  7282  exmidaclem  7320  djuenun  7324  exmidapne  7372  cc1  7377  cc2lem  7378  mulidnq  7502  ltsonq  7511  halfnqq  7523  nqnq0pi  7551  nq02m  7578  cauappcvgprlemm  7758  cauappcvgprlemloc  7765  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  cauappcvgprlem2  7773  cauappcvgpr  7775  ltposr  7876  0idsr  7880  1idsr  7881  mappsrprg  7917  ax1rid  7990  ax0id  7991  axpre-ltirr  7995  mulrid  8069  1p1times  8206  cnegexlem3  8249  pncan1  8449  npcan1  8450  kcnktkm1cn  8455  apirr  8678  recexap  8726  eqneg  8805  subrecap  8912  lediv2a  8968  nn1m1nn  9054  2txmxeqx  9168  subhalfhalf  9272  add1p1  9287  sub1m1  9288  cnm2m1cnm3  9289  xp1d2m1eqxm1d2  9290  div4p1lem1div2  9291  nn0addcl  9330  nn0mulcl  9331  zadd2cl  9502  nn0ledivnn  9889  nltpnft  9936  ngtmnft  9939  xrrebnd  9941  xnegneg  9955  xnegid  9981  xaddid1  9984  fzss1  10185  fzssp1  10189  fzshftral  10230  0elfz  10240  nn0fz0  10241  elfz0add  10242  fz0tp  10244  elfzoelz  10269  fzoval  10270  fzoss2  10296  fzossrbm1  10297  fzouzsplit  10303  elfzo1  10314  fzonn0p1  10340  fzossfzop1  10341  fzoend  10351  fzosplitsn  10362  fvinim0ffz  10370  2tnp1ge0ge0  10444  fldiv4p1lem1div2  10448  frec2uzltd  10548  frec2uzrand  10550  uzenom  10570  frecfzennn  10571  seqeq1  10595  iseqf1olemkle  10642  iseqf1olemklt  10643  iseqf1olemqk  10652  seq3f1olemstep  10659  seq3f1olemp  10660  seq3f1oleml  10661  seqf1oglem2  10665  seq3id  10670  seq3id2  10671  ser0f  10679  m1expcl2  10706  sqoddm1div8  10838  mulsubdivbinom2ap  10856  faclbnd  10886  facubnd  10890  bcpasc  10911  hashcl  10926  omgadd  10947  snopiswrd  11004  elovmpowrd  11035  lswwrd  11040  ccatval1  11053  ccatsymb  11058  ccatass  11064  ccat1st1st  11093  swrdf  11108  reval  11160  imval  11161  crim  11169  replim  11170  rexuz3  11301  absval  11312  sqrt0  11315  resqrexlemp1rp  11317  resqrexlemfp1  11320  resqrex  11337  abs00  11375  leabs  11385  absimle  11395  cau3  11426  dfabsmax  11528  climshft  11615  fsum3  11698  fsumcnv  11748  fsumiun  11788  binom  11795  bcxmaslem1  11799  isumshft  11801  arisum  11809  arisum2  11810  trireciplem  11811  trirecip  11812  geo2sum2  11826  geo2lim  11827  prodf1f  11854  prod0  11896  fprodfac  11926  ege2le3  11982  ef4p  12005  efgt1p2  12006  efgt1p  12007  sinval  12013  cosval  12014  negdvdsb  12118  dvdsnegb  12119  dvdsssfz1  12163  dvds1  12164  3dvds  12175  even2n  12185  oddge22np1  12192  2tp1odd  12195  ltoddhalfle  12204  m1expo  12211  m1exp1  12212  flodddiv4  12247  bits0e  12260  bits0o  12261  bitsp1e  12263  bitsp1o  12264  bitsfzo  12266  bitsinv1lem  12272  bitsinv1  12273  gcdsupex  12278  gcdsupcl  12279  alginv  12369  algcvg  12370  algcvga  12373  algfx  12374  eucalgcvga  12380  lcmdvds  12401  pw2dvds  12488  oddpwdclemodd  12494  phimul  12548  eulerth  12555  pc2dvds  12653  pcz  12655  pcmpt  12666  pcmptdvds  12668  fldivp1  12671  oddprmdvds  12677  pockthg  12680  pockthi  12681  1arith  12690  zgz  12696  4sqlem19  12732  evenennn  12764  ennnfonelemp1  12777  ennnfonelemkh  12783  ennnfonelemnn0  12793  ssnnctlemct  12817  strslfv2  12876  strslfv  12877  basm  12893  ressvalsets  12896  ressbasid  12902  pwsval  13123  qusex  13157  xpsfeq  13177  intopsn  13199  mgmidmo  13204  ismgmid  13209  mgmlrid  13211  lidrideqd  13213  lidrididd  13214  grpinvalem  13217  grpinva  13218  gsum0g  13228  issgrp  13235  imasmnd2  13284  mnd1  13287  mnd1id  13288  idmhm  13301  issubm  13304  0mhm  13318  resmhm  13319  resmhm2  13320  resmhm2b  13321  dfgrp2  13359  isgrpid2  13372  grpidd2  13373  grpinvval  13375  grpressid  13393  grpsubid1  13417  dfgrp3mlem  13430  grplactfval  13433  imasgrp2  13446  mhmlem  13450  mulgfvalg  13457  mulgnnp1  13466  mulgsubcl  13472  mulgnncl  13473  mulgnn0cl  13474  mulgcl  13475  mulgnn0z  13485  mulgneg2  13492  mulgmodid  13497  submmulg  13502  issubg  13509  subgid  13511  subgex  13512  subg0  13516  subginv  13517  subgcl  13520  subgsub  13522  subgmulg  13524  issubg3  13528  isnsg  13538  isnsg3  13543  nmzsubg  13546  nmznsg  13549  eqgval  13559  idghm  13595  resghm  13596  ghmnsgima  13604  ablressid  13671  mgpvalg  13685  rngressid  13716  ringressid  13825  imasring  13826  opprvalg  13831  opprsubgg  13846  dvdsrex  13860  dvdsrtr  13863  unitinvcl  13885  unitinvinv  13886  unitlinv  13888  unitrinv  13889  issubrng  13961  subrngid  13963  issubrng2  13972  issubrg  13983  subrgid  13985  issubrg2  14003  rrgval  14024  isdomn  14031  lmodlema  14054  islmodd  14055  rmodislmod  14113  lsssn0  14132  sraval  14199  sraring  14211  sralmod  14212  rlmvalg  14216  rlmbasg  14217  rlmplusgg  14218  rlm0g  14219  rlmsubg  14220  rlmmulrg  14221  rlmscabas  14222  rlmvscag  14223  rlmtopng  14224  rlmdsg  14225  rlmvnegg  14227  lidlss  14238  lidlssbas  14239  lidlbas  14240  crngridl  14292  zringinvg  14366  mulgrhm  14371  znval  14398  znf1o  14413  psrelbasfun  14439  mplvalcoe  14452  tsettps  14510  baspartn  14522  eltg  14524  en1top  14549  isopn3  14597  resttopon  14643  lmbr2  14686  cnptopresti  14710  cndis  14713  lmfpm  14715  lmcl  14717  lmff  14721  txswaphmeolem  14792  ispsmet  14795  psmet0  14799  xmetunirn  14830  bl2in  14875  metrest  14978  expcn  15041  cncfmptid  15069  negcncf  15077  negfcncf  15078  hovera  15119  hoverb  15120  limccl  15131  eldvap  15154  dvexp  15183  dvmptid  15188  dveflem  15198  dvef  15199  elply  15206  plypow  15216  dvply1  15237  logge0b  15362  logle1b  15364  logcxp  15369  fsumdvdsmul  15463  perfectlem2  15472  zabsle1  15476  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsdir2lem2  15506  lgsdir2lem4  15508  lgsdirnn0  15524  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  gausslemma2dlem1  15538  2lgslem1a1  15563  2lgslem1a2  15564  2lgslem1b  15566  2lgslem1c  15567  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgsoddprmlem2  15583  2lgsoddprmlem3d  15587  edgfndxid  15608  bj-ex  15698  bdth  15767  bj-indind  15868