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  628  notnot  630  con3i  633  biijust  642  con3  643  con2  644  pm5.19  708  olc  713  orc  714  pm2.621  749  pm1.2  758  orim1i  762  orim2i  763  pm2.41  778  pm2.42  779  pm2.4  780  pm4.44  781  orim2  791  orbi1  794  pm2.38  805  pm2.74  809  pm3.2ni  815  biort  831  dcbiit  841  pm4.79dc  905  dcand  935  biantr  955  3anim1i  1188  3anim2i  1189  3anim3i  1190  mpd3an23  1352  trujust  1375  tru  1377  dftru2  1381  truimtru  1429  falimfal  1432  3impexp  1458  19.26  1505  19.8a  1614  19.9ht  1665  ax6blem  1674  19.36i  1696  19.41h  1709  equsb1  1809  sbieh  1814  dveeq2or  1840  spsbim  1867  2ax17  1902  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  moanmo  2132  nfcvf  2372  neqne  2385  neneq  2399  necon3i  2425  nebidc  2457  r19.27v  2634  r19.28v  2635  vtoclgft  2825  rspcime  2888  eueq2dc  2950  cdeqcv  2996  ru  3001  sbcied2  3040  sbcralt  3079  sbcrext  3080  csbiebt  3137  csbied2  3145  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  ssid  3217  difss2  3305  ddifstab  3309  abvor0dc  3488  ssdifeq0  3547  rabsnt  3713  unisng  3873  dfnfc2  3874  ssbr  4095  a9evsep  4174  axnul  4177  rabex2  4198  intid  4276  opm  4286  opth1  4288  opth  4289  copsex4g  4299  0nelop  4300  moop2  4304  pocl  4358  swopo  4361  limeq  4432  suceq  4457  eusvnfb  4509  onintexmid  4629  nn0eln0  4676  elvvuni  4747  coss1  4841  coss2  4842  dmxpm  4907  elrnmpt1  4938  soirri  5086  relcnvtr  5211  relssdmrn  5212  cnvpom  5234  fveqeq2  5598  funopsn  5775  fvsng  5793  isose  5903  canth  5910  riota2f  5934  acexmidlemab  5951  fvoveq1  5980  0neqopab  6003  ssoprab2  6014  caovcld  6113  caovcomd  6116  caovassd  6119  caovcand  6122  caovordid  6126  caovordd  6128  caovdid  6135  caovdird  6138  caovimo  6153  f1opw  6166  caofref  6196  caofinvl  6197  caofid0l  6198  caofid0r  6199  xpexgALT  6231  op1stg  6249  op2ndg  6250  releldm2  6284  elopabi  6294  dfmpo  6322  smoeq  6389  tfr1onlemaccex  6447  tfrcllemaccex  6460  rdgisucinc  6484  rdg0g  6487  oacl  6559  nna0r  6577  nnmsucr  6587  ercnv  6654  swoord1  6662  swoord2  6663  eqer  6665  ider  6666  iinerm  6707  brecop  6725  ixpssmapg  6828  elixpsn  6835  en1bg  6905  fundmeng  6913  rex2dom  6924  xpsneng  6932  mapen  6958  phplem3g  6968  php5  6970  php5dom  6975  findcard2d  7003  findcard2sd  7004  undifdc  7036  xpfi  7044  elfir  7090  fi0  7092  ordiso2  7152  ctssdclemr  7229  nnnninfeq2  7246  nninfisol  7250  ctssexmid  7267  nninfinfwlpo  7297  exmidaclem  7336  djuenun  7340  exmidapne  7392  cc1  7397  cc2lem  7398  mulidnq  7522  ltsonq  7531  halfnqq  7543  nqnq0pi  7571  nq02m  7598  cauappcvgprlemm  7778  cauappcvgprlemloc  7785  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  cauappcvgprlem2  7793  cauappcvgpr  7795  ltposr  7896  0idsr  7900  1idsr  7901  mappsrprg  7937  ax1rid  8010  ax0id  8011  axpre-ltirr  8015  mulrid  8089  1p1times  8226  cnegexlem3  8269  pncan1  8469  npcan1  8470  kcnktkm1cn  8475  apirr  8698  recexap  8746  eqneg  8825  subrecap  8932  lediv2a  8988  nn1m1nn  9074  2txmxeqx  9188  subhalfhalf  9292  add1p1  9307  sub1m1  9308  cnm2m1cnm3  9309  xp1d2m1eqxm1d2  9310  div4p1lem1div2  9311  nn0addcl  9350  nn0mulcl  9351  zadd2cl  9522  nn0ledivnn  9909  nltpnft  9956  ngtmnft  9959  xrrebnd  9961  xnegneg  9975  xnegid  10001  xaddid1  10004  fzss1  10205  fzssp1  10209  fzshftral  10250  0elfz  10260  nn0fz0  10261  elfz0add  10262  fz0tp  10264  elfzoelz  10289  fzoval  10290  fzoss2  10316  fzossrbm1  10317  fzouzsplit  10323  elfzo1  10336  fzonn0p1  10362  fzossfzop1  10363  fzoend  10373  fzosplitsn  10384  fvinim0ffz  10392  2tnp1ge0ge0  10466  fldiv4p1lem1div2  10470  frec2uzltd  10570  frec2uzrand  10572  uzenom  10592  frecfzennn  10593  seqeq1  10617  iseqf1olemkle  10664  iseqf1olemklt  10665  iseqf1olemqk  10674  seq3f1olemstep  10681  seq3f1olemp  10682  seq3f1oleml  10683  seqf1oglem2  10687  seq3id  10692  seq3id2  10693  ser0f  10701  m1expcl2  10728  sqoddm1div8  10860  mulsubdivbinom2ap  10878  faclbnd  10908  facubnd  10912  bcpasc  10933  hashcl  10948  omgadd  10969  snopiswrd  11026  elovmpowrd  11057  lswwrd  11062  ccatval1  11076  ccatsymb  11081  ccatass  11087  ccat1st1st  11116  swrdf  11131  pfxsuff1eqwrdeq  11175  ccatpfx  11177  reval  11235  imval  11236  crim  11244  replim  11245  rexuz3  11376  absval  11387  sqrt0  11390  resqrexlemp1rp  11392  resqrexlemfp1  11395  resqrex  11412  abs00  11450  leabs  11460  absimle  11470  cau3  11501  dfabsmax  11603  climshft  11690  fsum3  11773  fsumcnv  11823  fsumiun  11863  binom  11870  bcxmaslem1  11874  isumshft  11876  arisum  11884  arisum2  11885  trireciplem  11886  trirecip  11887  geo2sum2  11901  geo2lim  11902  prodf1f  11929  prod0  11971  fprodfac  12001  ege2le3  12057  ef4p  12080  efgt1p2  12081  efgt1p  12082  sinval  12088  cosval  12089  negdvdsb  12193  dvdsnegb  12194  dvdsssfz1  12238  dvds1  12239  3dvds  12250  even2n  12260  oddge22np1  12267  2tp1odd  12270  ltoddhalfle  12279  m1expo  12286  m1exp1  12287  flodddiv4  12322  bits0e  12335  bits0o  12336  bitsp1e  12338  bitsp1o  12339  bitsfzo  12341  bitsinv1lem  12347  bitsinv1  12348  gcdsupex  12353  gcdsupcl  12354  alginv  12444  algcvg  12445  algcvga  12448  algfx  12449  eucalgcvga  12455  lcmdvds  12476  pw2dvds  12563  oddpwdclemodd  12569  phimul  12623  eulerth  12630  pc2dvds  12728  pcz  12730  pcmpt  12741  pcmptdvds  12743  fldivp1  12746  oddprmdvds  12752  pockthg  12755  pockthi  12756  1arith  12765  zgz  12771  4sqlem19  12807  evenennn  12839  ennnfonelemp1  12852  ennnfonelemkh  12858  ennnfonelemnn0  12868  ssnnctlemct  12892  strslfv2  12951  strslfv  12952  basm  12968  ressvalsets  12971  ressbasid  12977  pwsval  13198  qusex  13232  xpsfeq  13252  intopsn  13274  mgmidmo  13279  ismgmid  13284  mgmlrid  13286  lidrideqd  13288  lidrididd  13289  grpinvalem  13292  grpinva  13293  gsum0g  13303  issgrp  13310  imasmnd2  13359  mnd1  13362  mnd1id  13363  idmhm  13376  issubm  13379  0mhm  13393  resmhm  13394  resmhm2  13395  resmhm2b  13396  dfgrp2  13434  isgrpid2  13447  grpidd2  13448  grpinvval  13450  grpressid  13468  grpsubid1  13492  dfgrp3mlem  13505  grplactfval  13508  imasgrp2  13521  mhmlem  13525  mulgfvalg  13532  mulgnnp1  13541  mulgsubcl  13547  mulgnncl  13548  mulgnn0cl  13549  mulgcl  13550  mulgnn0z  13560  mulgneg2  13567  mulgmodid  13572  submmulg  13577  issubg  13584  subgid  13586  subgex  13587  subg0  13591  subginv  13592  subgcl  13595  subgsub  13597  subgmulg  13599  issubg3  13603  isnsg  13613  isnsg3  13618  nmzsubg  13621  nmznsg  13624  eqgval  13634  idghm  13670  resghm  13671  ghmnsgima  13679  ablressid  13746  mgpvalg  13760  rngressid  13791  ringressid  13900  imasring  13901  opprvalg  13906  opprsubgg  13921  dvdsrex  13935  dvdsrtr  13938  unitinvcl  13960  unitinvinv  13961  unitlinv  13963  unitrinv  13964  issubrng  14036  subrngid  14038  issubrng2  14047  issubrg  14058  subrgid  14060  issubrg2  14078  rrgval  14099  isdomn  14106  lmodlema  14129  islmodd  14130  rmodislmod  14188  lsssn0  14207  sraval  14274  sraring  14286  sralmod  14287  rlmvalg  14291  rlmbasg  14292  rlmplusgg  14293  rlm0g  14294  rlmsubg  14295  rlmmulrg  14296  rlmscabas  14297  rlmvscag  14298  rlmtopng  14299  rlmdsg  14300  rlmvnegg  14302  lidlss  14313  lidlssbas  14314  lidlbas  14315  crngridl  14367  zringinvg  14441  mulgrhm  14446  znval  14473  znf1o  14488  psrelbasfun  14514  mplvalcoe  14527  tsettps  14585  baspartn  14597  eltg  14599  en1top  14624  isopn3  14672  resttopon  14718  lmbr2  14761  cnptopresti  14785  cndis  14788  lmfpm  14790  lmcl  14792  lmff  14796  txswaphmeolem  14867  ispsmet  14870  psmet0  14874  xmetunirn  14905  bl2in  14950  metrest  15053  expcn  15116  cncfmptid  15144  negcncf  15152  negfcncf  15153  hovera  15194  hoverb  15195  limccl  15206  eldvap  15229  dvexp  15258  dvmptid  15263  dveflem  15273  dvef  15274  elply  15281  plypow  15291  dvply1  15312  logge0b  15437  logle1b  15439  logcxp  15444  fsumdvdsmul  15538  perfectlem2  15547  zabsle1  15551  lgsval  15556  lgsfvalg  15557  lgsval2lem  15562  lgsdir2lem2  15581  lgsdir2lem4  15583  lgsdirnn0  15599  gausslemma2dlem0i  15609  gausslemma2dlem1a  15610  gausslemma2dlem1  15613  2lgslem1a1  15638  2lgslem1a2  15639  2lgslem1b  15641  2lgslem1c  15642  2lgslem3a  15645  2lgslem3b  15646  2lgslem3c  15647  2lgslem3d  15648  2lgsoddprmlem2  15658  2lgsoddprmlem3d  15662  edgfndxid  15683  uhgr0e  15753  bj-ex  15837  bdth  15905  bj-indind  16006