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-06.)

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 560  orim2 566  pm2.38 567  orbi1 618  anbi1 619  pm4.22 620  imbi1 621  bibi1 623  pm5.36 649  exmid 653  biantr 740  orbidi 741  bimsc1 748  con3th 764  consensus 765  mpd3an23 915  ax6 976  19.20 991  hba1 1000  cbv3 1160  cbval 1161  equsb1 1189  sbie 1192  moanmo 1424  necon3i 1597  ralcom2 1768  eueq2 1909  ru 1928  csbiegft 2019  unisng 2508  axnul 2699  dtruALT 2738  copsex4g 2784  opthwiener 2796  pwundif 2817  pocl 2835  sucidg 3042  ordunisuc 3079  onsucuni2 3081  onuninsuc 3098  unizlim 3103  orduninsuc 3104  elvvuni 3219  ssrel 3237  dmxpid 3322  sotri 3429  relssdr 3499  cnvpo 3508  fvopab4gf 3766  fvopabgf 3772  fvopabnf 3773  fvi 3827  canth 3892  rdg0t 3929  abianfplem 3946  abianfp 3947  caoprmo 4056  op1stg 4071  op2ndg 4072  1st2val 4079  2nd2val 4080  curry1val 4084  oesuc 4150  oa0r 4157  om1r 4161  omordi 4181  oeworde 4204  oelim2 4206  nnmsucr 4224  oaabs 4236  nneob 4239  eqer 4255  xpsneng 4416  limensuc 4487  inf3lema 4581  inf3lem2 4586  infensuc 4610  rankonid 4667  rankr1id 4669  aceq3lem 4704  aceq5 4712  ac6lem 4726  numthlem 4755  numth 4756  zorn2 4768  unidom 4780  unxpdomlem 4815  carduni 4830  cardiun 4831  cardprc 4833  alephle 4856  cardalephex 4858  alephfp2 4873  alephval3 4875  dominf 4876  cardcf 4883  mulidpq 5041  distrlem5pr 5103  0idsr 5178  1idsr 5179  ax0id 5253  ax1id 5254  cnegextlem3 5319  negnegt 5365  subid1t 5368  msqgt0t 5589  msqge0t 5590  lesub0t 5651  recext 5657  divcan1z 5687  divcan2z 5688  divcan1t 5689  divcan2t 5690  recidt 5698  divasst 5704  divcan3z 5716  divcan3t 5718  div1t 5729  recrect 5732  eqneg 5760  eqnegt 5761  lediv12it 5844  lediv2it 5845  xrmax1 5857  xrmin2 5860  max1ALT 5864  2timest 5951  halfpost 5983  xrub 6027  supxrmnf 6034  elnn0z 6094  qrecclt 6211  qbtwnxr 6217  om2uzlt 6235  seq1lem1 6246  seq1res 6264  elioo4g 6318  elfz2nn0t 6427  fzshftralt 6454  seqzfveq 6486  expord2t 6535  sq01t 6582  discrlem2 6587  nn0opth 6596  nn0opth2t 6598  sqrlem21 6623  sqrth 6629  sqrsqt 6652  sqsqrt 6653  cru 6667  crne0 6670  absvalt 6694  cjrebt 6735  cjmulrclt 6736  cjmulvalt 6737  cjmulge0t 6738  cjcjt 6746  addcjt 6750  absidt 6797  leabst 6799  abslem2 6846  faclbnd 6882  faclbnd4lem2 6886  faclbnd4lem3 6887  fsumsplit 6958  fsumcom 6966  fsumrev 6967  fsummulc1 6971  climsub 7066  geolim1 7174  cvgratlem2ALT 7183  cvgratlem2 7186  elcncf1i 7206  efaddlem10 7289  efsubt 7313  ef1tlub 7324  ef01tlub 7327  absef01tlub 7329  abspef01tlub 7336  efm1legeot 7358  efcnlem4 7362  acdc3lem 7428  acdc2lem1 7430  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  eltgt 7560  cldval 7608  islp 7685  metcnf 7823  metidcn 7839  causs 7890  lmfexlem2 7892  metelcls 7900  fsumcnlem 7923  lmcau 7930  bcthlem2 7934  bcthlem15 7947  bcthlem21 7953  bcthlem27 7959  isgrp 7975  grpidinvlem1 7982  grpidinvlem2 7983  grpidinvlem3 7984  grpidinv 7986  grpideu 7987  grpidinv2 7994  ablnncan 8049  grpsn 8061  cnid 8064  ringid 8082  ringsn 8100  vcid 8107  nvi 8173  nvelbl2 8264  nvcnf 8265  nvcni 8266  sqcn 8270  ipfval 8286  lnocoi 8352  nmlnoubi 8388  ipasslem5 8425  ipdi 8434  ipsubdi 8440  pythi 8441  htthlem8 8557  isps 8571  spwval2 8577  effoi 8666  effoiOLD 8667  normlem9at 8908  normsqt 8922  normpyth 8930  hhssnv 9054  pjthlem8 9141  ococt 9163  axpjpjt 9171  shsel3t 9194  shscl 9196  chocint 9333  chj0t 9335  chlejb1t 9350  chnlet 9352  chjot 9353  elspansn2t 9406  cmbrt 9444  cmbr3t 9468  pjoml2t 9471  pjoml3t 9472  cm2jt 9480  pjch1t 9532  pjinormt 9549  pjcht 9556  pjoi0t 9579  hoaddid1t 9634  hodidt 9635  eigret 9678  nmopub2tALT 9750  nmfnleub2t 9766  eigvalt 9800  lnopm 9840  lnopco 9843  lnopeq0 9847  lnopeq 9848  lnopunilem1 9850  lnophmlem1 9856  lnophmt 9859  hmopcot 9863  cnlnadjlem2 9916  adjmult 9939  branmfnt 9951  rnbra 9953  hmopidmch 9990  hmopidmpj 9991  hmopidmcht 9992  hmopidmpjt 9993  pjssge0t 10005  pjdifnormt 10006  pjsspos 10011  pjhmopidm 10020  dfpjopt 10021  pjclem4 10037  pj3s 10045  hstoht 10069  hstrlem3a 10097  mdslle1 10152  mdslle2 10153  mdslmd2 10165  csmdsym 10169  cvmdt 10171  cvexcht 10209  atexcht 10216  irredlem2 10226  irredlem3 10227  ghomgrp 10295  and4as 10332  faimpex 10339  moec 10357  idhme 10409  cnvhmph 10414  subsp 10429  isfil 10433  eloi 10503  1ded 10515  idosd 10521  1cat 10536  cmpida 10551  cmpidb 10552  ishomb 10560  eqidob 10567  ispgrag 10615

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

Copyright terms: Public domain