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	⊢ (φ → φ)

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-1 4	. 2 ⊢ (φ → (φ → φ))
2		ax-1 4	. 2 ⊢ (φ → ((φ → φ) → φ))
3	1, 2	mpd 26	1 ⊢ (φ → φ)

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 2514  axnul 2705  dtruALT 2744  copsex4g 2790  opthwiener 2804  pwundif 2825  pocl 2843  sucidg 3052  ordunisuc 3089  onsucuni2 3091  onuninsuc 3108  unizlim 3113  orduninsuc 3114  elvvuni 3229  ssrel 3247  dmxpid 3333  sotri 3443  relssdr 3514  cnvpo 3524  fvopab4gf 3783  fvopabgf 3789  fvopabnf 3790  fvi 3844  canth 3909  rdg0t 3946  abianfplem 3963  abianfp 3964  caoprmo 4073  op1stg 4088  op2ndg 4089  1st2val 4096  2nd2val 4097  curry1val 4101  oesuc 4167  oa0r 4174  om1r 4178  omordi 4198  oeworde 4221  oelim2 4223  nnmsucr 4241  oaabs 4253  nneob 4256  eqer 4272  xpsneng 4433  limensuc 4505  inf3lema 4601  inf3lem2 4606  infensuc 4630  rankonid 4687  rankr1id 4689  aceq3lem 4724  aceq5 4732  ac6lem 4746  numthlem 4775  numth 4776  zorn2 4788  unidom 4800  unxpdomlem 4835  carduni 4850  cardiun 4851  cardprc 4853  alephle 4876  cardalephex 4878  alephfp2 4893  alephval3 4895  dominf 4896  cardcf 4903  mulidpq 5061  distrlem5pr 5123  0idsr 5198  1idsr 5199  ax0id 5273  ax1id 5274  cnegextlem3 5339  negnegt 5385  subid1t 5388  msqgt0t 5609  msqge0t 5610  lesub0t 5671  recext 5677  divcan1z 5707  divcan2z 5708  divcan1t 5709  divcan2t 5710  recidt 5718  divasst 5724  divcan3z 5736  divcan3t 5738  div1t 5749  recrect 5752  eqneg 5780  eqnegt 5781  lediv12it 5864  lediv2it 5865  xrmax1 5877  xrmin2 5880  max1ALT 5884  2timest 5971  halfpost 6003  xrub 6047  supxrmnf 6054  elnn0z 6114  qrecclt 6231  qbtwnxr 6237  om2uzlt 6255  seq1lem1 6266  seq1res 6284  elioo4g 6338  elfz2nn0t 6447  fzshftralt 6474  seqzfveq 6506  expord2t 6555  sq01t 6602  discrlem2 6607  nn0opth 6616  nn0opth2t 6618  sqrlem21 6643  sqrth 6649  sqrsqt 6672  sqsqrt 6673  cru 6687  crne0 6690  absvalt 6714  cjrebt 6755  cjmulrclt 6756  cjmulvalt 6757  cjmulge0t 6758  cjcjt 6766  addcjt 6770  absidt 6817  leabst 6819  abslem2 6866  faclbnd 6902  faclbnd4lem2 6906  faclbnd4lem3 6907  fsumsplit 6978  fsumcom 6986  fsumrev 6987  fsummulc1 6991  climsub 7086  geolim1 7194  cvgratlem2ALT 7203  cvgratlem2 7206  elcncf1i 7226  efaddlem10 7309  efsubt 7333  ef1tlub 7344  ef01tlub 7347  absef01tlub 7349  abspef01tlub 7356  efm1legeot 7378  efcnlem4 7382  acdc3lem 7448  acdc2lem1 7450  acdc2lem2 7451  acdc5lem2 7454  acdclem 7456  eltgt 7580  cldval 7628  islp 7706  metcnf 7848  metidcn 7864  causs 7918  lmfexlem2 7920  metelcls 7928  fsumcnlem 7951  lmcau 7958  bcthlem2 7962  bcthlem15 7975  bcthlem21 7981  bcthlem27 7987  isgrp 8003  grpidinvlem1 8010  grpidinvlem2 8011  grpidinvlem3 8012  grpidinv 8014  grpideu 8015  grpidinv2 8022  ablnncan 8077  grpsn 8089  cnid 8092  ringid 8110  ringsn 8128  vcid 8135  nvi 8201  nvelbl2 8293  nvcnf 8294  nvcni 8295  sqcn 8299  ipfval 8315  lnocoi 8381  nmlnoubi 8417  ipasslem5 8454  ipdi 8463  ipsubdi 8469  pythi 8470  htthlem8 8586  isps 8604  spwval2 8611  effoi 8701  effoiOLD 8702  normlem9at 8961  normsqt 8975  normpyth 8983  hhssnv 9108  pjthlem8 9199  ococt 9221  axpjpjt 9229  shsel3t 9252  shscl 9254  chocint 9391  chj0t 9393  chlejb1t 9408  chnlet 9410  chjot 9411  elspansn2t 9464  cmbrt 9502  cmbr3t 9526  pjoml2t 9529  pjoml3t 9530  cm2jt 9538  pjch1t 9590  pjinormt 9607  pjcht 9614  pjoi0t 9637  hoaddid1t 9692  hodidt 9693  eigret 9736  nmopub2tALT 9808  nmfnleub2t 9824  eigvalt 9858  lnopm 9898  lnopco 9901  lnopeq0 9905  lnopeq 9906  lnopunilem1 9908  lnophmlem1 9914  lnophmt 9917  hmopcot 9921  cnlnadjlem2 9974  adjmult 9998  branmfnt 10011  rnbra 10013  hmopidmch 10052  hmopidmpj 10053  hmopidmcht 10054  hmopidmpjt 10055  pjssge0t 10067  pjdifnormt 10068  pjsspos 10073  pjhmopidm 10083  dfpjopt 10084  pjclem4 10100  pj3s 10108  hstoht 10132  hstrlem3a 10160  mdslle1 10215  mdslle2 10216  mdslmd2 10228  csmdsym 10232  cvmdt 10234  cvexcht 10272  atexcht 10279  irredlem2 10289  irredlem3 10290  ghomgrp 10358  and4as 10404  faimpex 10411  moec 10429  idhme 10481  cnvhmph 10486  subsp 10501  isfil 10505  eloi 10575  1ded 10587  idosd 10593  1cat 10608  cmpida 10623  cmpidb 10624  ishomb 10632  eqidob 10639  ispgrag 10687

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

Copyright terms: Public domain