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  4167  axnul  4170  rabex2  4191  intid  4269  opm  4279  opth1  4281  opth  4282  copsex4g  4292  0nelop  4293  moop2  4297  pocl  4351  swopo  4354  limeq  4425  suceq  4450  eusvnfb  4502  onintexmid  4622  nn0eln0  4669  elvvuni  4740  coss1  4834  coss2  4835  dmxpm  4899  elrnmpt1  4930  soirri  5078  relcnvtr  5203  relssdmrn  5204  cnvpom  5226  fveqeq2  5587  funopsn  5764  fvsng  5782  isose  5892  canth  5899  riota2f  5923  acexmidlemab  5940  fvoveq1  5969  0neqopab  5992  ssoprab2  6003  caovcld  6102  caovcomd  6105  caovassd  6108  caovcand  6111  caovordid  6115  caovordd  6117  caovdid  6124  caovdird  6127  caovimo  6142  f1opw  6155  caofref  6185  caofinvl  6186  caofid0l  6187  caofid0r  6188  xpexgALT  6220  op1stg  6238  op2ndg  6239  releldm2  6273  elopabi  6283  dfmpo  6311  smoeq  6378  tfr1onlemaccex  6436  tfrcllemaccex  6449  rdgisucinc  6473  rdg0g  6476  oacl  6548  nna0r  6566  nnmsucr  6576  ercnv  6643  swoord1  6651  swoord2  6652  eqer  6654  ider  6655  iinerm  6696  brecop  6714  ixpssmapg  6817  elixpsn  6824  en1bg  6894  fundmeng  6901  rex2dom  6912  xpsneng  6919  mapen  6945  phplem3g  6955  php5  6957  php5dom  6962  findcard2d  6990  findcard2sd  6991  undifdc  7023  xpfi  7031  elfir  7077  fi0  7079  ordiso2  7139  ctssdclemr  7216  nnnninfeq2  7233  nninfisol  7237  ctssexmid  7254  nninfinfwlpo  7284  exmidaclem  7322  djuenun  7326  exmidapne  7374  cc1  7379  cc2lem  7380  mulidnq  7504  ltsonq  7513  halfnqq  7525  nqnq0pi  7553  nq02m  7580  cauappcvgprlemm  7760  cauappcvgprlemloc  7767  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  cauappcvgprlem2  7775  cauappcvgpr  7777  ltposr  7878  0idsr  7882  1idsr  7883  mappsrprg  7919  ax1rid  7992  ax0id  7993  axpre-ltirr  7997  mulrid  8071  1p1times  8208  cnegexlem3  8251  pncan1  8451  npcan1  8452  kcnktkm1cn  8457  apirr  8680  recexap  8728  eqneg  8807  subrecap  8914  lediv2a  8970  nn1m1nn  9056  2txmxeqx  9170  subhalfhalf  9274  add1p1  9289  sub1m1  9290  cnm2m1cnm3  9291  xp1d2m1eqxm1d2  9292  div4p1lem1div2  9293  nn0addcl  9332  nn0mulcl  9333  zadd2cl  9504  nn0ledivnn  9891  nltpnft  9938  ngtmnft  9941  xrrebnd  9943  xnegneg  9957  xnegid  9983  xaddid1  9986  fzss1  10187  fzssp1  10191  fzshftral  10232  0elfz  10242  nn0fz0  10243  elfz0add  10244  fz0tp  10246  elfzoelz  10271  fzoval  10272  fzoss2  10298  fzossrbm1  10299  fzouzsplit  10305  elfzo1  10316  fzonn0p1  10342  fzossfzop1  10343  fzoend  10353  fzosplitsn  10364  fvinim0ffz  10372  2tnp1ge0ge0  10446  fldiv4p1lem1div2  10450  frec2uzltd  10550  frec2uzrand  10552  uzenom  10572  frecfzennn  10573  seqeq1  10597  iseqf1olemkle  10644  iseqf1olemklt  10645  iseqf1olemqk  10654  seq3f1olemstep  10661  seq3f1olemp  10662  seq3f1oleml  10663  seqf1oglem2  10667  seq3id  10672  seq3id2  10673  ser0f  10681  m1expcl2  10708  sqoddm1div8  10840  mulsubdivbinom2ap  10858  faclbnd  10888  facubnd  10892  bcpasc  10913  hashcl  10928  omgadd  10949  snopiswrd  11006  elovmpowrd  11037  lswwrd  11042  ccatval1  11056  ccatsymb  11061  ccatass  11067  ccat1st1st  11096  swrdf  11111  pfxsuff1eqwrdeq  11153  ccatpfx  11155  reval  11193  imval  11194  crim  11202  replim  11203  rexuz3  11334  absval  11345  sqrt0  11348  resqrexlemp1rp  11350  resqrexlemfp1  11353  resqrex  11370  abs00  11408  leabs  11418  absimle  11428  cau3  11459  dfabsmax  11561  climshft  11648  fsum3  11731  fsumcnv  11781  fsumiun  11821  binom  11828  bcxmaslem1  11832  isumshft  11834  arisum  11842  arisum2  11843  trireciplem  11844  trirecip  11845  geo2sum2  11859  geo2lim  11860  prodf1f  11887  prod0  11929  fprodfac  11959  ege2le3  12015  ef4p  12038  efgt1p2  12039  efgt1p  12040  sinval  12046  cosval  12047  negdvdsb  12151  dvdsnegb  12152  dvdsssfz1  12196  dvds1  12197  3dvds  12208  even2n  12218  oddge22np1  12225  2tp1odd  12228  ltoddhalfle  12237  m1expo  12244  m1exp1  12245  flodddiv4  12280  bits0e  12293  bits0o  12294  bitsp1e  12296  bitsp1o  12297  bitsfzo  12299  bitsinv1lem  12305  bitsinv1  12306  gcdsupex  12311  gcdsupcl  12312  alginv  12402  algcvg  12403  algcvga  12406  algfx  12407  eucalgcvga  12413  lcmdvds  12434  pw2dvds  12521  oddpwdclemodd  12527  phimul  12581  eulerth  12588  pc2dvds  12686  pcz  12688  pcmpt  12699  pcmptdvds  12701  fldivp1  12704  oddprmdvds  12710  pockthg  12713  pockthi  12714  1arith  12723  zgz  12729  4sqlem19  12765  evenennn  12797  ennnfonelemp1  12810  ennnfonelemkh  12816  ennnfonelemnn0  12826  ssnnctlemct  12850  strslfv2  12909  strslfv  12910  basm  12926  ressvalsets  12929  ressbasid  12935  pwsval  13156  qusex  13190  xpsfeq  13210  intopsn  13232  mgmidmo  13237  ismgmid  13242  mgmlrid  13244  lidrideqd  13246  lidrididd  13247  grpinvalem  13250  grpinva  13251  gsum0g  13261  issgrp  13268  imasmnd2  13317  mnd1  13320  mnd1id  13321  idmhm  13334  issubm  13337  0mhm  13351  resmhm  13352  resmhm2  13353  resmhm2b  13354  dfgrp2  13392  isgrpid2  13405  grpidd2  13406  grpinvval  13408  grpressid  13426  grpsubid1  13450  dfgrp3mlem  13463  grplactfval  13466  imasgrp2  13479  mhmlem  13483  mulgfvalg  13490  mulgnnp1  13499  mulgsubcl  13505  mulgnncl  13506  mulgnn0cl  13507  mulgcl  13508  mulgnn0z  13518  mulgneg2  13525  mulgmodid  13530  submmulg  13535  issubg  13542  subgid  13544  subgex  13545  subg0  13549  subginv  13550  subgcl  13553  subgsub  13555  subgmulg  13557  issubg3  13561  isnsg  13571  isnsg3  13576  nmzsubg  13579  nmznsg  13582  eqgval  13592  idghm  13628  resghm  13629  ghmnsgima  13637  ablressid  13704  mgpvalg  13718  rngressid  13749  ringressid  13858  imasring  13859  opprvalg  13864  opprsubgg  13879  dvdsrex  13893  dvdsrtr  13896  unitinvcl  13918  unitinvinv  13919  unitlinv  13921  unitrinv  13922  issubrng  13994  subrngid  13996  issubrng2  14005  issubrg  14016  subrgid  14018  issubrg2  14036  rrgval  14057  isdomn  14064  lmodlema  14087  islmodd  14088  rmodislmod  14146  lsssn0  14165  sraval  14232  sraring  14244  sralmod  14245  rlmvalg  14249  rlmbasg  14250  rlmplusgg  14251  rlm0g  14252  rlmsubg  14253  rlmmulrg  14254  rlmscabas  14255  rlmvscag  14256  rlmtopng  14257  rlmdsg  14258  rlmvnegg  14260  lidlss  14271  lidlssbas  14272  lidlbas  14273  crngridl  14325  zringinvg  14399  mulgrhm  14404  znval  14431  znf1o  14446  psrelbasfun  14472  mplvalcoe  14485  tsettps  14543  baspartn  14555  eltg  14557  en1top  14582  isopn3  14630  resttopon  14676  lmbr2  14719  cnptopresti  14743  cndis  14746  lmfpm  14748  lmcl  14750  lmff  14754  txswaphmeolem  14825  ispsmet  14828  psmet0  14832  xmetunirn  14863  bl2in  14908  metrest  15011  expcn  15074  cncfmptid  15102  negcncf  15110  negfcncf  15111  hovera  15152  hoverb  15153  limccl  15164  eldvap  15187  dvexp  15216  dvmptid  15221  dveflem  15231  dvef  15232  elply  15239  plypow  15249  dvply1  15270  logge0b  15395  logle1b  15397  logcxp  15402  fsumdvdsmul  15496  perfectlem2  15505  zabsle1  15509  lgsval  15514  lgsfvalg  15515  lgsval2lem  15520  lgsdir2lem2  15539  lgsdir2lem4  15541  lgsdirnn0  15557  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  gausslemma2dlem1  15571  2lgslem1a1  15596  2lgslem1a2  15597  2lgslem1b  15599  2lgslem1c  15600  2lgslem3a  15603  2lgslem3b  15604  2lgslem3c  15605  2lgslem3d  15606  2lgsoddprmlem2  15616  2lgsoddprmlem3d  15620  edgfndxid  15641  bj-ex  15735  bdth  15804  bj-indind  15905