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

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜑 → (𝜑 → 𝜑))
2		ax-1 6	. 2 ⊢ (𝜑 → ((𝜑 → 𝜑) → 𝜑))
3	1, 2	mpd 13	1 ⊢ (𝜑 → 𝜑)

Syntax hints:   → wi 4

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

This theorem is referenced by:  idd  21  2a1  25  com12  30  pm2.27  40  pm2.43i  49  pm2.43d  50  pm2.43a  51  imim2  55  imim1i  60  imim1  76  pm2.04  82  pm2.86  101  biimprd  158  biimpcd  159  biimprcd  160  biid  171  bibi2i  227  imbi1  236  imbi2  237  bibi1  240  pm3.3  261  pm3.31  262  jctl  314  jctr  315  ancli  323  ancri  324  anc2li  329  anc2ri  330  anim12i  338  anim1i  340  anim1ci  341  anim2i  342  pm4.24  395  anass  401  mpdan  421  mpancom  422  pm5.32  453  anbi1  466  anbi2  467  mpan10  474  adantl3r  512  simpll  527  simplr  528  simprl  529  simprr  531  pm3.45  597  pm5.36  610  con2i  627  notnot  629  con3i  632  biijust  641  con3  642  con2  643  pm5.19  706  olc  711  orc  712  pm2.621  747  pm1.2  756  orim1i  760  orim2i  761  pm2.41  776  pm2.42  777  pm2.4  778  pm4.44  779  orim2  789  orbi1  792  pm2.38  803  pm2.74  807  pm3.2ni  813  biort  829  dcbiit  839  pm4.79dc  903  biantr  952  3anim1i  1185  3anim2i  1186  3anim3i  1187  mpd3an23  1339  trujust  1355  tru  1357  dftru2  1361  truimtru  1409  falimfal  1412  3impexp  1437  19.26  1481  19.8a  1590  19.9ht  1641  ax6blem  1650  19.36i  1672  19.41h  1685  equsb1  1785  sbieh  1790  dveeq2or  1816  spsbim  1843  2ax17  1878  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  moanmo  2103  nfcvf  2342  neqne  2355  neneq  2369  necon3i  2395  nebidc  2427  r19.27v  2604  r19.28v  2605  vtoclgft  2789  rspcime  2850  eueq2dc  2912  cdeqcv  2958  ru  2963  sbcied2  3002  sbcralt  3041  sbcrext  3042  csbiebt  3098  csbied2  3106  cbvralcsf  3121  cbvrexcsf  3122  cbvreucsf  3123  cbvrabcsf  3124  ssid  3177  difss2  3265  ddifstab  3269  abvor0dc  3448  ssdifeq0  3507  rabsnt  3669  unisng  3828  dfnfc2  3829  a9evsep  4127  axnul  4130  intid  4226  opm  4236  opth1  4238  opth  4239  copsex4g  4249  0nelop  4250  moop2  4253  pocl  4305  swopo  4308  limeq  4379  suceq  4404  eusvnfb  4456  onintexmid  4574  nn0eln0  4621  elvvuni  4692  coss1  4784  coss2  4785  dmxpm  4849  elrnmpt1  4880  soirri  5025  relcnvtr  5150  relssdmrn  5151  cnvpom  5173  fveqeq2  5526  fvsng  5714  isose  5824  canth  5831  riota2f  5854  acexmidlemab  5871  fvoveq1  5900  0neqopab  5922  ssoprab2  5933  caovcld  6030  caovcomd  6033  caovassd  6036  caovcand  6039  caovordid  6043  caovordd  6045  caovdid  6052  caovdird  6055  caovimo  6070  f1opw  6080  caofref  6106  caofinvl  6107  xpexgALT  6136  op1stg  6153  op2ndg  6154  releldm2  6188  elopabi  6198  dfmpo  6226  smoeq  6293  tfr1onlemaccex  6351  tfrcllemaccex  6364  rdgisucinc  6388  rdg0g  6391  oacl  6463  nna0r  6481  nnmsucr  6491  ercnv  6558  swoord1  6566  swoord2  6567  eqer  6569  ider  6570  iinerm  6609  brecop  6627  ixpssmapg  6730  elixpsn  6737  en1bg  6802  fundmeng  6809  xpsneng  6824  mapen  6848  phplem3g  6858  php5  6860  php5dom  6865  findcard2d  6893  findcard2sd  6894  undifdc  6925  xpfi  6931  elfir  6974  fi0  6976  ordiso2  7036  ctssdclemr  7113  nnnninfeq2  7129  nninfisol  7133  ctssexmid  7150  exmidaclem  7209  djuenun  7213  exmidapne  7261  cc1  7266  cc2lem  7267  mulidnq  7390  ltsonq  7399  halfnqq  7411  nqnq0pi  7439  nq02m  7466  cauappcvgprlemm  7646  cauappcvgprlemloc  7653  cauappcvgprlemladdru  7657  cauappcvgprlemladdrl  7658  cauappcvgprlem2  7661  cauappcvgpr  7663  ltposr  7764  0idsr  7768  1idsr  7769  mappsrprg  7805  ax1rid  7878  ax0id  7879  axpre-ltirr  7883  mulrid  7956  1p1times  8093  cnegexlem3  8136  pncan1  8336  npcan1  8337  kcnktkm1cn  8342  apirr  8564  recexap  8612  eqneg  8691  subrecap  8798  lediv2a  8854  nn1m1nn  8939  add1p1  9170  sub1m1  9171  cnm2m1cnm3  9172  xp1d2m1eqxm1d2  9173  div4p1lem1div2  9174  nn0addcl  9213  nn0mulcl  9214  zadd2cl  9384  nn0ledivnn  9769  nltpnft  9816  ngtmnft  9819  xrrebnd  9821  xnegneg  9835  xnegid  9861  xaddid1  9864  fzss1  10065  fzssp1  10069  fzshftral  10110  0elfz  10120  nn0fz0  10121  elfz0add  10122  fz0tp  10124  elfzoelz  10149  fzoval  10150  fzoss2  10174  fzossrbm1  10175  fzouzsplit  10181  elfzo1  10192  fzonn0p1  10213  fzossfzop1  10214  fzoend  10224  fzosplitsn  10235  fvinim0ffz  10243  2tnp1ge0ge0  10303  fldiv4p1lem1div2  10307  frec2uzltd  10405  frec2uzrand  10407  uzenom  10427  frecfzennn  10428  seqeq1  10450  iseqf1olemkle  10486  iseqf1olemklt  10487  iseqf1olemqk  10496  seq3f1olemstep  10503  seq3f1olemp  10504  seq3f1oleml  10505  seq3id  10510  seq3id2  10511  ser0f  10517  m1expcl2  10544  sqoddm1div8  10676  mulsubdivbinom2ap  10693  faclbnd  10723  facubnd  10727  bcpasc  10748  hashcl  10763  omgadd  10784  reval  10860  imval  10861  crim  10869  replim  10870  rexuz3  11001  absval  11012  sqrt0  11015  resqrexlemp1rp  11017  resqrexlemfp1  11020  resqrex  11037  abs00  11075  leabs  11085  absimle  11095  cau3  11126  dfabsmax  11228  climshft  11314  fsum3  11397  fsumcnv  11447  fsumiun  11487  binom  11494  bcxmaslem1  11498  isumshft  11500  arisum  11508  arisum2  11509  trireciplem  11510  trirecip  11511  geo2sum2  11525  geo2lim  11526  prodf1f  11553  prod0  11595  fprodfac  11625  ege2le3  11681  ef4p  11704  efgt1p2  11705  efgt1p  11706  sinval  11712  cosval  11713  negdvdsb  11816  dvdsnegb  11817  dvdsssfz1  11860  dvds1  11861  even2n  11881  oddge22np1  11888  2tp1odd  11891  ltoddhalfle  11900  m1expo  11907  m1exp1  11908  flodddiv4  11941  gcdsupex  11960  gcdsupcl  11961  alginv  12049  algcvg  12050  algcvga  12053  algfx  12054  eucalgcvga  12060  lcmdvds  12081  pw2dvds  12168  oddpwdclemodd  12174  phimul  12228  eulerth  12235  pc2dvds  12331  pcz  12333  pcmpt  12343  pcmptdvds  12345  fldivp1  12348  oddprmdvds  12354  pockthg  12357  pockthi  12358  1arith  12367  zgz  12373  evenennn  12396  ennnfonelemp1  12409  ennnfonelemkh  12415  ennnfonelemnn0  12425  ssnnctlemct  12449  strslfv2  12508  strslfv  12509  ressvalsets  12526  xpsfeq  12769  intopsn  12791  mgmidmo  12796  ismgmid  12801  mgmlrid  12803  lidrideqd  12805  lidrididd  12806  grprinvlem  12809  grprinvd  12810  issgrp  12814  mnd1  12852  mnd1id  12853  idmhm  12865  issubm  12868  0mhm  12878  dfgrp2  12907  isgrpid2  12918  grpidd2  12919  grpinvval  12921  grpressid  12936  grpsubid1  12960  dfgrp3mlem  12973  grplactfval  12976  mhmlem  12983  mulgfvalg  12990  mulgnnp1  12996  mulgsubcl  13002  mulgnncl  13003  mulgnn0cl  13004  mulgcl  13005  mulgnn0z  13015  mulgneg2  13022  mulgmodid  13027  issubg  13038  subgid  13040  subgex  13041  subg0  13045  subginv  13046  subgcl  13049  subgsub  13051  subgmulg  13053  issubg3  13057  isnsg  13067  isnsg3  13072  nmzsubg  13075  nmznsg  13078  eqgval  13087  mgpvalg  13138  ringressid  13243  opprvalg  13246  dvdsrex  13272  dvdsrtr  13275  unitinvcl  13297  unitinvinv  13298  unitlinv  13300  unitrinv  13301  issubrg  13347  subrgid  13349  issubrg2  13367  lmodlema  13387  islmodd  13388  rmodislmod  13446  lsssn0  13461  zringinvg  13533  tsettps  13577  baspartn  13589  eltg  13591  en1top  13616  isopn3  13664  resttopon  13710  lmbr2  13753  cnptopresti  13777  cndis  13780  lmfpm  13782  lmcl  13784  lmff  13788  txswaphmeolem  13859  ispsmet  13862  psmet0  13866  xmetunirn  13897  bl2in  13942  metrest  14045  cncfmptid  14122  negcncf  14127  negfcncf  14128  limccl  14167  eldvap  14190  dvexp  14214  dveflem  14226  dvef  14227  logge0b  14350  logle1b  14352  logcxp  14357  zabsle1  14439  lgsval  14444  lgsfvalg  14445  lgsval2lem  14450  lgsdir2lem2  14469  lgsdir2lem4  14471  lgsdirnn0  14487  2lgsoddprmlem2  14493  2lgsoddprmlem3d  14497  bj-ex  14553  bdth  14622  bj-indind  14723