Theorem id 73

Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 74. (The proof was shortened by Stefan Allan, 20-Mar-2006.)

Assertion

Ref	Expression
id	|- (ph -> ph)

Proof of Theorem id

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

Syntax hints:   -> wi 3

This theorem is referenced by:  idd 75  pm2.27 76  pm2.43i 78  pm2.43d 79  pm2.43a 80  bijust 161  biid 186  jctl 312  jctr 313  ancli 318  ancri 319  anim1i 359  anim2i 360  orim1i 362  orim2i 363  pm2.41 367  pm2.42 368  pm2.4 369  pm4.44 370  simpll 446  simplr 447  simprl 448  simprr 449  pm3.45 618  orim2 624  pm2.38 625  orbi1 679  anbi1 680  bitr 681  imbi1 682  bibi1 684  pm5.36 710  exmid 714  biantr 811  orbidi 812  bimsc1 820  con3th 840  consensus 841  consensusOLD 842  prlem2 847  3anim1i 933  3anim3i 934  mpd3an23 1040  iidn3 1114  bitr3 1125  idi 1132  ax6 1163  alim 1178  hba1 1188  19.41 1286  cbv3 1363  cbvalOLD 1366  equsb1 1399  sbie 1403  2ax17 1505  moanmo 1668  necon3i 1877  nebi 1919  ralcom2OLD 2079  eueq2 2262  ru 2284  csbiegft 2406  ssid 2467  unisng 3016  axnul 3259  elOLD 3301  dtru 3313  intid 3327  copsex4g 3355  opthwiener 3369  pwundif 3394  pocl 3411  limeq 3484  suceq 3544  sucidg 3560  unizlim 3597  ordunisuc 3722  ordunisucOLD 3723  onsucuni2OLD 3726  onuninsuci 3732  orduninsuc 3736  vtoclrbr 3844  elvvuni 3866  ssrelOLD 3887  ssrelrelOLD 3895  dmxpid 3990  sotri 4126  relssdmrn 4227  cnvpo 4238  funss 4250  fvopab4gf 4555  fvopabgf 4561  fvopabnf 4562  fvi 4629  caoprmo 4814  op1stg 4839  op2ndg 4840  1st2val 4849  2nd2val 4850  iunfoprab 4883  curry1val 4888  curry2val 4891  canth 4923  rdg0g 4963  abianfplem 4981  abianfp 4982  oesuc 5022  oa0r 5031  om1r 5035  omordi 5056  oeworde 5079  oelim2 5081  nnmsucr 5106  nnmsucrOLD 5107  oaabs 5120  nneob 5123  eqer 5140  xpsneng 5306  limensuc 5411  ordiso 5493  elirr 5511  inf3lema 5524  inf3lem2 5529  infensuc 5554  en3lplem2 5566  rankonid 5615  rankr1id 5617  omsubindss 5684  aceq3lem 5690  aceq5 5698  ac6lem 5712  numthlem 5741  numth 5742  zorn2 5754  unidom 5766  unxpdomlem 5791  carduni 5806  cardiun 5807  cardprc 5809  alephle 5828  cardalephex 5830  alephfp2 5845  alephval3 5847  dominf 5848  cardcf 5855  mulidpq 6017  distrlem5pr 6079  0idsr 6154  1idsr 6155  ax0id 6230  ax1id 6231  cnegexlem3 6297  negneg 6349  subid1 6352  msqgt0 6593  msqge0 6594  lesub0 6663  recex 6672  divcan1zi 6703  divcan2zi 6704  divcan1 6705  recid 6714  divcan3zi 6732  divcan3 6734  div1 6745  recrec 6748  eqnegi 6777  eqneg 6778  ltmul2OLD 6805  lemul1OLD 6807  lemul2OLD 6809  lemul1aOLD 6815  lediv1OLD 6829  ltmuldiv2OLD 6843  ltdivmulOLD 6845  ledivmulOLD 6847  lt2mul2divOLD 6850  ledivmul2OLD 6852  lemuldiv2OLD 6855  lediv12a 6874  lediv2a 6875  xrmax1 6887  xrmin2 6890  max1ALT 6894  2times 6983  halfpos 7017  xrub 7084  supxrmnf 7091  elnn0z 7151  qdivcl 7249  qbtwnxr 7255  modval 7296  elfz2nn0 7462  fztp 7481  fzshftral 7496  om2uzlti 7504  seq1lem1 7517  seq1res 7535  seqzfveq 7592  exprec 7632  expsubOLD 7637  expord2 7644  sq01 7692  discrlem2 7702  nn0opthi 7711  nn0opth2 7713  sqrlem21 7738  sqrthi 7744  sqrsq 7767  sqsqr 7768  crui 7782  crne0i 7784  absval 7807  cjreb 7845  cjmulrcl 7846  cjmulval 7847  cjmulge0 7848  cjcj 7856  addcj 7860  absid 7908  leabs 7910  abslem2 7956  faclbnd 7992  faclbnd4lem2 7996  faclbnd4lem3 7997  fsumsplit 8075  fsumcom 8083  fsumrev 8084  fsummulc1 8088  climsub 8185  geolim1 8296  cvgratlem2 8308  elcncf1ii 8328  efaddlem10 8404  efaddlem23 8417  ef1tlubi 8439  ef01tlubi 8443  absef01tlubi 8445  abspef01tlubi 8455  efm1legeo 8478  efcnlem4 8482  acdc3lem 8549  acdc2lem1 8552  acdc2lem2 8553  acdc5lem2 8556  acdclem 8558  eltg 8683  cldval 8737  islp 8815  metcnf 8957  metidcn 8973  causs 9028  lmfexlem2 9030  metelcls 9038  fsumcnlem 9062  lmcau 9069  bcthlem2 9073  bcthlem15 9086  bcthlem21 9092  bcthlem27 9098  isgrp 9116  grpidinvlem1 9123  grpidinvlem2 9124  grpidinvlem3 9125  grpidinv 9127  grpideu 9128  grpsn 9135  grpidinv2 9139  ablnncan 9215  cnid 9230  ga0 9248  gagrpid 9253  ringid 9264  ringideu 9265  ringsn 9285  drngi 9288  vcid 9297  nvi 9360  nvelbl2 9453  nvcnf 9454  nvcni 9456  nvcni2 9457  sqcn 9469  ipfval 9486  lnocoi 9552  nmlnoubi 9591  ishmo 9606  ipasslem5 9630  ipdi 9639  ipsubdi 9645  pythi 9646  htthlem8 9769  isps 9783  spwval2 9791  effoi 9894  subsp 10036  stoig 10043  stoig2 10044  isfil 10058  flimfnei 10111  iscon 10131  iscon2 10132  isdir 10144  opidon 10161  isexid2 10164  exidu1 10165  cmpidelt 10168  rngmgmbs4 10193  normlem9at 10412  normsq 10426  normpythi 10434  hhssnv 10559  pjthlem8 10651  ococ 10673  axpjpj 10681  shsel3 10704  shscli 10706  chocin 10843  chj0 10845  chlejb1 10860  chnle 10862  chjo 10863  elspansn2 10915  cmbr 10952  cmbr3 10976  pjoml2 10979  pjoml3 10980  cm2j 10988  pjch1 11042  pjinormi 11059  pjch 11066  pjoi0 11089  hoaddid1 11146  hodid 11147  eigre 11190  nmopub2tALT 11262  nmfnleub2 11279  eigval1 11313  lnopmi 11354  lnopcoi 11357  lnopeq0i 11361  lnopeqi 11362  lnopunilem1 11364  lnophmlem1 11370  lnophm 11373  hmopco 11377  cnlnadjlem2 11430  adjmul 11454  branmfn 11467  branmfnOLD 11468  rnbra 11470  opsqrlem1 11503  opsqrlem4 11506  hmopidmchi 11515  hmopidmpji 11516  hmopidmch 11517  hmopidmpj 11518  pjssge0i 11530  pjdifnormi 11531  pjssposi 11536  pjhmopidm 11546  dfpjop 11547  pjclem4 11564  pj3si 11572  hstoh 11596  hstrlem3a 11624  dmdbr5 11672  mdslle1i 11681  mdslle2i 11682  mdslmd2i 11694  csmdsymi 11698  cvmd 11700  cvexch 11738  atexch 11745  irredlem2 11755  irredlem3 11756  bnj1051 12682  bnj1235 12796  bnj1247 12805  bnj1254 12810  bnj944 13132  bnj950 13134  bnj1367 13303  bnj1450 13333  bnj1463 13342  bnj1529 13366  bnj1530 13367  fndmeng 13390  ghomgrp 13425  negdvdsb 13463  dvdsnegb 13464  muldvds1 13470  muldvds2 13471  dvds2add 13477  dvds2sub 13478  gcdaddm 13527  algfx 13540  eucalgval 13541  mulgcd 13555  frr3g 13772  FFIid 13847  tbw-bijust 13895  and4as 13996  facrm 14018  r19.2zrr 14024  moec 14079  eloi 14130  rnxpid 14139  reltrncnv 14186  injsurinj 14214  islatalg 14257  labss1 14263  labss2 14265  gepsup 14316  seinf 14317  mxlelt2 14328  mnlelt2 14330  defselem 14336  inposet 14344  istoset2 14353  fprodp1s1 14407  ridlideq 14419  mgmlion 14420  fincmpzer 14434  ltlga 14452  curgrpact 14458  fprodneg 14464  fprodsub 14465  ununr 14492  fldi 14499  vecval1b 14517  vecval3b 14518  vri 14557  osneisi 14596  idhme 14599  cnvhmph 14601  eqindhome 14615  topgele 14629  fbfgss2 14651  clsingemp 14675  istopgrp 14685  idtrgrp 14692  cntrsetlem 14709  1ded 14767  idosd 14773  1cat 14788  cmpida 14803  cmpidb 14804  dualded 14814  dualcat2 14815  eqidob 14826  cinvlem2 14859  idsubfun 14888  isplibg1 14991  isplibg3 14995  isplibg4a 14997  isplibg4b 14999  3com12d 15029  fictblem 15052  ordisoOLD 15056  omsubindssOLD 15079  opnregcld 15097  cldregopn 15098  compsub 15113  hscptsscld 15116  alexsublem3 15121  alexsublem4 15122  alexsub 15123  dfcon2 15124  2ndc1stc 15159  fneint 15168  topfne 15182  comppfsc 15199  neibastop2lem3 15203  isufil 15246  ufprim 15251  isfclusf 15307  flfssfcf 15311  welb 15441  supclt 15444  rddif 15480  absrdbnd 15481  seq1p1g 15487  seqzp1g 15489  sdclem1 15491  sdc 15493  lpss2 15524  caures 15534  constcncf 15564  txmet 15607  sstotbnd 15618  bfplem8 15687  bfplem10 15689  rrntotbnd 15704  reheibor 15707  phtpycom 15732  phtpycolem3 15735  phtpycolem4 15736  phtpyco 15738  reparpht 15747  pcofval 15754  pcoval 15755  pcohtpylem3 15764  pcorev 15769  pi1bval 15770  elpi1 15771  pi1gp 15777  flddmn 15888  ispgrag 15983  2alim 16011  pm11.58 16029  ax4567to6 16044  ax4567to7 16045  cbvralcsf 16093  cbvrexcsf 16094  cbvreucsf 16095  cbvrabcsf 16096  smoeq 16126  smoge 16136  idn1 16142  trsspwALT2 16300  sspwtrALT 16303  pwtrr 16308  sstrALT2 16318  tpid3gVD 16325  bitr3VD 16332  19.21a3con13vVD 16335  exbirVD 16336  idiVD 16347  posref 16534  posgeref 16554  isopos 16664  oposlem 16668  cmtval 16690  omllaw 16715  leatom 16754  hlrelat2 16793  grpidinvlem1NEW 16838  grpidinvlem2NEW 16839  grpidinvlem3NEW 16840  grpidinvNEW 16842  grpideuNEW 16843  grpidinv2NEW 16848  ringideuNEW 16875  ringidmlemNEW 16882  issrng 16905  islvec 16917  iscsubsp 16938

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain