Theorem id 19

Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see idALT 20. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Assertion

Ref	Expression
id	|- ( ph -> ph )

Proof of Theorem id

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

Syntax hints:   -> wi 4

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

This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  39  pm2.43i  48  pm2.43d  49  pm2.43a  50  imim2  54  imim1i  59  imim1  75  pm2.04  81  pm2.86  99  biimprd  156  biimpcd  157  biimprcd  158  biid  169  bibi2i  225  imbi1  234  imbi2  235  bibi1  238  pm3.3  257  pm3.31  258  jctl  307  jctr  308  ancli  316  ancri  317  anc2li  322  anc2ri  323  anim12i  331  anim1i  333  anim2i  334  pm4.24  387  anass  393  mpdan  412  mpancom  413  pm5.32  440  anbi1  453  anbi2  454  mpan10  457  simpll  495  simplr  496  simprl  497  simprr  498  pm3.45  561  pm5.36  574  con2i  589  notnot  591  con3i  594  biijust  602  con3  603  con2  604  notbii  626  pm5.19  654  olc  664  orc  665  pm2.621  698  pm1.2  705  orim1i  709  orim2i  710  pm2.41  725  pm2.42  726  pm2.4  727  pm4.44  728  orim2  735  orbi1  738  pm2.38  749  pm2.74  753  pm3.2ni  759  pm4.79dc  842  biantr  893  3anim1i  1124  3anim2i  1125  3anim3i  1126  mpd3an23  1270  trujust  1286  tru  1288  dftru2  1292  truimtru  1340  falimfal  1343  3impexp  1366  19.26  1410  19.8a  1522  19.9ht  1572  ax6blem  1580  19.36i  1602  19.41h  1615  equsb1  1708  sbieh  1713  dveeq2or  1737  spsbim  1764  2ax17  1799  dvelimALT  1927  dvelimfv  1928  dvelimor  1935  moanmo  2018  nfcvf  2240  neqne  2253  neneq  2267  necon3i  2293  nebidc  2325  vtoclgft  2649  eueq2dc  2765  cdeqcv  2809  ru  2814  sbcied2  2851  sbcralt  2890  sbcrext  2891  csbiebt  2942  csbied2  2949  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  ssid  3018  difss2  3100  ddifstab  3104  abvor0dc  3269  ssdifeq0  3325  ifbi  3369  rabsnt  3467  unisng  3618  dfnfc2  3619  a9evsep  3900  axnul  3903  intid  3979  opm  3989  opth1  3991  opth  3992  copsex4g  4002  0nelop  4003  moop2  4006  pocl  4058  swopo  4061  limeq  4132  suceq  4157  eusvnfb  4204  onintexmid  4315  nn0eln0  4359  elvvuni  4422  coss1  4509  coss2  4510  dmxpm  4573  elrnmpt1  4603  soirri  4739  relcnvtr  4860  relssdmrn  4861  cnvpom  4880  fvsng  5380  isose  5480  riota2f  5509  acexmidlemab  5526  0neqopab  5570  ssoprab2  5581  caovcld  5674  caovcomd  5677  caovassd  5680  caovcand  5683  caovordid  5687  caovordd  5689  caovdid  5696  caovdird  5699  caovimo  5714  grprinvlem  5715  grprinvd  5716  f1opw  5727  caofref  5752  caofinvl  5753  xpexgALT  5780  op1stg  5797  op2ndg  5798  releldm2  5831  elopabi  5841  dfmpt2  5864  smoeq  5928  rdgisucinc  5995  rdg0g  5998  oacl  6063  nna0r  6080  nnmsucr  6090  ercnv  6150  swoord1  6158  swoord2  6159  eqer  6161  ider  6162  iinerm  6201  brecop  6219  en1bg  6303  fundmeng  6310  xpsneng  6319  phplem3g  6342  php5  6344  php5dom  6349  findcard2d  6375  findcard2sd  6376  ordiso2  6446  mulidnq  6579  ltsonq  6588  halfnqq  6600  nqnq0pi  6628  nq02m  6655  cauappcvgprlemm  6835  cauappcvgprlemloc  6842  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem2  6850  cauappcvgpr  6852  ltposr  6940  0idsr  6944  1idsr  6945  ax1rid  7043  ax0id  7044  axpre-ltirr  7048  mulid1  7116  1p1times  7242  cnegexlem3  7285  pncan1  7481  npcan1  7482  kcnktkm1cn  7487  apirr  7705  recexap  7743  eqneg  7820  lediv2a  7973  nn1m1nn  8057  add1p1  8280  sub1m1  8281  cnm2m1cnm3  8282  xp1d2m1eqxm1d2  8283  div4p1lem1div2  8284  nn0addcl  8323  nn0mulcl  8324  zadd2cl  8476  nn0ledivnn  8838  nltpnft  8884  ngtmnft  8885  xrrebnd  8886  xnegneg  8900  fzss1  9081  fzssp1  9085  fzshftral  9125  0elfz  9132  nn0fz0  9133  elfz0add  9134  fz0tp  9135  elfzoelz  9157  fzoval  9158  fzoss2  9181  fzossrbm1  9182  fzouzsplit  9188  elfzo1  9199  fzonn0p1  9220  fzossfzop1  9221  fzoend  9231  fzosplitsn  9242  fvinim0ffz  9250  2tnp1ge0ge0  9303  fldiv4p1lem1div2  9307  frec2uzltd  9405  frec2uzrand  9407  uzenom  9418  frecfzennn  9419  iseqeq1  9434  iseqid  9467  iser0f  9472  m1expcl2  9498  sqoddm1div8  9625  faclbnd  9668  facubnd  9672  bcpasc  9693  reval  9736  imval  9737  crim  9745  replim  9746  rexuz3  9876  absval  9887  sqrt0  9890  resqrexlemp1rp  9892  resqrexlemfp1  9895  resqrex  9912  leabs  9960  absimle  9970  cau3  10001  dfabsmax  10103  climshft  10143  negdvdsb  10211  dvdsnegb  10212  dvdsssfz1  10252  dvds1  10253  even2n  10273  oddge22np1  10281  2tp1odd  10284  ltoddhalfle  10293  m1expo  10300  m1exp1  10301  flodddiv4  10334  gcdsupex  10349  gcdsupcl  10350  ialginv  10429  ialgcvg  10430  ialgcvga  10433  ialgfx  10434  eucialgcvga  10440  lcmdvds  10461  pw2dvds  10544  oddpwdclemodd  10550  bj-ex  10573  bdth  10622  bj-dcbi  10719  bj-indind  10727