Theorem id 59

Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 60. (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 26	1 |- (ph -> ph)

Syntax hints:   -> wi 3

This theorem is referenced by:  idd 61  pm2.27 62  bijust 145  pm4.2 170  jctl 290  jctr 291  ancli 296  ancri 297  anim1i 334  anim2i 335  orim1i 337  orim2i 338  pm2.41 342  pm2.42 343  pm2.4 344  pm4.44 345  simpll 412  simplr 413  simprl 414  simprr 415  pm3.45 561  orim2 567  pm2.38 568  orbi1 619  anbi1 620  pm4.22 621  imbi1 622  bibi1 624  pm5.36 650  exmid 654  biantr 741  orbidi 742  bimsc1 749  con3th 765  consensus 766  mpd3an23 916  ax6 977  19.20 992  hba1 1001  cbv3 1162  cbval 1163  equsb1 1191  sbie 1194  moanmo 1429  necon3i 1602  ralcom2 1773  eueq2 1914  ru 1934  csbiegft 2025  unisng 2513  axnul 2704  dtruALT 2743  copsex4g 2789  opthwiener 2802  pwundif 2823  pocl 2839  sucidg 3047  ordunisuc 3084  onsucuni2 3086  onuninsuc 3103  unizlim 3108  orduninsuc 3109  elvvuni 3224  ssrel 3242  dmxpid 3328  sotri 3435  relssdr 3505  cnvpo 3514  fvopab4gf 3772  fvopabgf 3778  fvopabnf 3779  fvi 3833  canth 3898  rdg0t 3935  abianfplem 3952  abianfp 3953  caoprmo 4062  op1stg 4077  op2ndg 4078  1st2val 4085  2nd2val 4086  curry1val 4090  oesuc 4156  oa0r 4163  om1r 4167  omordi 4187  oeworde 4210  oelim2 4212  nnmsucr 4230  oaabs 4242  nneob 4245  eqer 4261  xpsneng 4422  limensuc 4493  inf3lema 4589  inf3lem2 4594  infensuc 4618  rankonid 4675  rankr1id 4677  aceq3lem 4712  aceq5 4720  ac6lem 4734  numthlem 4763  numth 4764  zorn2 4776  unidom 4788  unxpdomlem 4823  carduni 4838  cardiun 4839  cardprc 4841  alephle 4864  cardalephex 4866  alephfp2 4881  alephval3 4883  dominf 4884  cardcf 4891  mulidpq 5049  distrlem5pr 5111  0idsr 5186  1idsr 5187  ax0id 5261  ax1id 5262  cnegextlem3 5327  negnegt 5373  subid1t 5376  msqgt0t 5597  msqge0t 5598  lesub0t 5659  recext 5665  divcan1z 5695  divcan2z 5696  divcan1t 5697  divcan2t 5698  recidt 5706  divasst 5712  divcan3z 5724  divcan3t 5726  div1t 5737  recrect 5740  eqneg 5768  eqnegt 5769  lediv12it 5852  lediv2it 5853  xrmax1 5865  xrmin2 5868  max1ALT 5872  2timest 5959  halfpost 5991  xrub 6035  supxrmnf 6042  elnn0z 6102  qrecclt 6219  qbtwnxr 6225  om2uzlt 6243  seq1lem1 6254  seq1res 6272  elioo4g 6326  elfz2nn0t 6435  fzshftralt 6462  seqzfveq 6494  expord2t 6543  sq01t 6590  discrlem2 6595  nn0opth 6604  nn0opth2t 6606  sqrlem21 6631  sqrth 6637  sqrsqt 6660  sqsqrt 6661  cru 6675  crne0 6678  absvalt 6702  cjrebt 6743  cjmulrclt 6744  cjmulvalt 6745  cjmulge0t 6746  cjcjt 6754  addcjt 6758  absidt 6805  leabst 6807  abslem2 6854  faclbnd 6890  faclbnd4lem2 6894  faclbnd4lem3 6895  fsumsplit 6966  fsumcom 6974  fsumrev 6975  fsummulc1 6979  climsub 7074  geolim1 7182  cvgratlem2ALT 7191  cvgratlem2 7194  elcncf1i 7214  efaddlem10 7297  efsubt 7321  ef1tlub 7332  ef01tlub 7335  absef01tlub 7337  abspef01tlub 7344  efm1legeot 7366  efcnlem4 7370  acdc3lem 7436  acdc2lem1 7438  acdc2lem2 7439  acdc5lem2 7442  acdclem 7444  eltgt 7568  cldval 7616  islp 7694  metcnf 7836  metidcn 7852  causs 7906  lmfexlem2 7908  metelcls 7916  fsumcnlem 7939  lmcau 7946  bcthlem2 7950  bcthlem15 7963  bcthlem21 7969  bcthlem27 7975  isgrp 7991  grpidinvlem1 7998  grpidinvlem2 7999  grpidinvlem3 8000  grpidinv 8002  grpideu 8003  grpidinv2 8010  ablnncan 8064  grpsn 8076  cnid 8079  ringid 8097  ringsn 8115  vcid 8122  nvi 8185  nvelbl2 8277  nvcnf 8278  nvcni 8279  sqcn 8283  ipfval 8299  lnocoi 8365  nmlnoubi 8401  ipasslem5 8438  ipdi 8447  ipsubdi 8453  pythi 8454  htthlem8 8570  isps 8588  spwval2 8595  effoi 8684  normlem9at 8926  normsqt 8940  normpyth 8948  hhssnv 9073  pjthlem8 9164  ococt 9186  axpjpjt 9194  shsel3t 9217  shscl 9219  chocint 9356  chj0t 9358  chlejb1t 9373  chnlet 9375  chjot 9376  elspansn2t 9429  cmbrt 9467  cmbr3t 9491  pjoml2t 9494  pjoml3t 9495  cm2jt 9503  pjch1t 9555  pjinormt 9572  pjcht 9579  pjoi0t 9602  hoaddid1t 9657  hodidt 9658  eigret 9701  nmopub2tALT 9773  nmfnleub2t 9789  eigvalt 9823  lnopm 9863  lnopco 9866  lnopeq0 9870  lnopeq 9871  lnopunilem1 9873  lnophmlem1 9879  lnophmt 9882  hmopcot 9886  cnlnadjlem2 9939  adjmult 9963  branmfnt 9976  rnbra 9978  hmopidmch 10017  hmopidmpj 10018  hmopidmcht 10019  hmopidmpjt 10020  pjssge0t 10032  pjdifnormt 10033  pjsspos 10038  pjhmopidm 10048  dfpjopt 10049  pjclem4 10065  pj3s 10073  hstoht 10097  hstrlem3a 10125  mdslle1 10181  mdslle2 10182  mdslmd2 10194  csmdsym 10198  cvmdt 10200  cvexcht 10238  atexcht 10245  irredlem2 10255  irredlem3 10256  ghomgrp 10324  and4as 10368  faimpex 10375  moec 10393  idhme 10445  cnvhmph 10450  subsp 10465  isfil 10469  eloi 10539  1ded 10551  idosd 10557  1cat 10572  cmpida 10587  cmpidb 10588  ishomb 10596  eqidob 10603  ispgrag 10651

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

Copyright terms: Public domain