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 562  orim2 568  pm2.38 569  orbi1 620  anbi1 621  pm4.22 622  imbi1 623  bibi1 625  pm5.36 651  exmid 655  biantr 742  orbidi 743  bimsc1 750  con3th 766  consensus 767  mpd3an23 918  ax6 979  19.20 994  hba1 1003  cbv3 1164  cbval 1165  equsb1 1193  sbie 1196  moanmo 1431  necon3i 1604  ralcom2 1775  eueq2 1916  ru 1936  csbiegft 2027  unisng 2516  axnul 2707  dtruALT 2746  copsex4g 2792  opthwiener 2805  pwundif 2826  pocl 2842  sucidg 3050  ordunisuc 3087  onsucuni2 3089  onuninsuc 3106  unizlim 3111  orduninsuc 3112  elvvuni 3227  ssrel 3245  dmxpid 3331  sotri 3441  relssdr 3511  cnvpo 3520  fvopab4gf 3779  fvopabgf 3785  fvopabnf 3786  fvi 3840  canth 3905  rdg0t 3942  abianfplem 3959  abianfp 3960  caoprmo 4068  op1stg 4085  op2ndg 4086  1st2val 4093  2nd2val 4094  curry1val 4098  oesuc 4164  oa0r 4171  om1r 4175  omordi 4195  oeworde 4218  oelim2 4220  nnmsucr 4238  oaabs 4250  nneob 4253  eqer 4269  xpsneng 4430  limensuc 4501  inf3lema 4597  inf3lem2 4602  infensuc 4626  rankonid 4683  rankr1id 4685  aceq3lem 4720  aceq5 4728  ac6lem 4742  numthlem 4771  numth 4772  zorn2 4784  unidom 4796  unxpdomlem 4831  carduni 4846  cardiun 4847  cardprc 4849  alephle 4872  cardalephex 4874  alephfp2 4889  alephval3 4891  dominf 4892  cardcf 4899  mulidpq 5057  distrlem5pr 5119  0idsr 5194  1idsr 5195  ax0id 5269  ax1id 5270  cnegextlem3 5335  negnegt 5381  subid1t 5384  msqgt0t 5603  msqge0t 5604  lesub0t 5665  recext 5671  divcan1z 5701  divcan2z 5702  divcan1t 5703  divcan2t 5704  recidt 5712  divasst 5718  divcan3z 5731  divcan3t 5733  div1t 5744  recrect 5747  eqneg 5775  eqnegt 5776  lediv12it 5864  lediv2it 5865  xrmax1 5877  xrmin2 5880  max1ALT 5884  2timest 5972  halfpost 6004  xrub 6048  supxrmnf 6055  elnn0z 6115  qrecclt 6237  qbtwnxr 6243  om2uzlt 6262  seq1lem1 6273  seq1res 6291  elioo4g 6345  elfz2nn0t 6455  fzshftralt 6482  seqzfveq 6514  expord2t 6564  sq01t 6611  discrlem2 6617  nn0opth 6626  nn0opth2t 6628  sqrlem21 6653  sqrth 6659  sqrsqt 6682  sqsqrt 6683  cru 6697  crne0 6699  absvalt 6722  cjrebt 6758  cjmulrclt 6759  cjmulvalt 6760  cjmulge0t 6761  cjcjt 6769  addcjt 6773  absidt 6820  leabst 6822  abslem2 6867  faclbnd 6903  faclbnd4lem2 6907  faclbnd4lem3 6908  fsumsplit 6978  fsumcom 6986  fsumrev 6987  fsummulc1 6991  climsub 7088  geolim1 7197  cvgratlem2ALT 7206  cvgratlem2 7209  elcncf1i 7229  efaddlem10 7305  efsubt 7329  ef1tlub 7340  ef01tlub 7344  absef01tlub 7346  abspef01tlub 7353  efm1legeot 7375  efcnlem4 7379  acdc3lem 7443  acdc2lem1 7445  acdc2lem2 7446  acdc5lem2 7449  acdclem 7451  eltgt 7575  cldval 7623  islp 7701  metcnf 7841  metidcn 7857  causs 7912  lmfexlem2 7914  metelcls 7922  fsumcnlem 7946  lmcau 7953  bcthlem2 7957  bcthlem15 7970  bcthlem21 7976  bcthlem27 7982  isgrp 7998  grpidinvlem1 8005  grpidinvlem2 8006  grpidinvlem3 8007  grpidinv 8009  grpideu 8010  grpidinv2 8017  ablnncan 8069  grpsn 8081  cnid 8084  ringid 8102  ringsn 8120  vcid 8127  nvi 8190  nvelbl2 8283  nvcnf 8284  nvcni 8286  nvcni2 8287  sqcn 8292  ipfval 8309  lnocoi 8375  nmlnoubi 8413  ipasslem5 8451  ipdi 8460  ipsubdi 8466  pythi 8467  htthlem8 8584  isps 8602  spwval2 8610  effoi 8700  normlem9at 8942  normsqt 8956  normpyth 8964  hhssnv 9089  pjthlem8 9181  ococt 9203  axpjpjt 9211  shsel3t 9234  shscl 9236  chocint 9373  chj0t 9375  chlejb1t 9390  chnlet 9392  chjot 9393  elspansn2t 9445  cmbrt 9482  cmbr3t 9506  pjoml2t 9509  pjoml3t 9510  cm2jt 9518  pjch1t 9570  pjinormt 9587  pjcht 9594  pjoi0t 9617  hoaddid1t 9672  hodidt 9673  eigret 9716  nmopub2tALT 9788  nmfnleub2t 9805  eigvalt 9839  lnopm 9880  lnopco 9883  lnopeq0 9887  lnopeq 9888  lnopunilem1 9890  lnophmlem1 9896  lnophmt 9899  hmopcot 9903  cnlnadjlem2 9956  adjmult 9980  branmfnt 9993  rnbra 9995  hmopidmch 10034  hmopidmpj 10035  hmopidmcht 10036  hmopidmpjt 10037  pjssge0t 10049  pjdifnormt 10050  pjsspos 10055  pjhmopidm 10065  dfpjopt 10066  pjclem4 10082  pj3s 10090  hstoht 10114  hstrlem3a 10142  dmdbr5 10190  mdslle1 10199  mdslle2 10200  mdslmd2 10212  csmdsym 10216  cvmdt 10218  cvexcht 10256  atexcht 10263  irredlem2 10273  irredlem3 10274  ghomgrp 10345  and4as 10386  faimpex 10393  moec 10411  idhme 10464  cnvhmph 10469  subsp 10484  isfil 10488  eloi 10571  1ded 10583  idosd 10589  1cat 10604  cmpida 10619  cmpidb 10620  ishomb 10628  eqidob 10635  ispgrag 10684

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

Copyright terms: Public domain