MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq2 Structured version   Visualization version   GIF version

Theorem eqeq2 2616
Description: Equality implies equivalence of equalities. (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Assertion
Ref Expression
eqeq2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))

Proof of Theorem eqeq2
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
21eqeq2d 2615 1 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-cleq 2598
This theorem is referenced by:  eqeq2i  2617  eqeq12  2618  alexeqg  3297  pm13.183  3308  eqeu  3339  moeq3  3345  mo2icl  3347  mob2  3348  euind  3355  reu6i  3359  reu2eqd  3365  reuind  3373  sbc2or  3406  sbc5  3422  csbiebg  3517  eqif  4071  sneq  4130  preq1b  4308  preqr1OLD  4311  prel12  4314  preq12bg  4317  prel12g  4318  preqsn  4322  disji2  4559  disjprg  4568  dtruALT  4817  dtruALT2  4829  opth  4861  euotd  4887  solin  4968  ideqg  5179  resieq  5310  cnveqb  5490  cnveq0  5491  iota5  5770  funopg  5818  fneq2  5876  foeq3  6007  tz6.12f  6103  funbrfv  6125  fnbrfvb  6127  fvelimab  6144  elrnrexdm  6252  fconst5  6350  eufnfv  6369  f1veqaeq  6392  isosolem  6471  mpt2eq123  6586  ovmpt4g  6655  ov3  6669  ovg  6671  caovcang  6706  caovcan  6709  tfisi  6923  tfindsg  6925  findsg  6958  f1oweALT  7016  seqomlem2  7406  oawordeu  7495  omopth  7598  ereq2  7610  qsdisj  7684  eroveu  7702  2dom  7888  fundmen  7889  xpf1o  7980  nneneq  8001  cantnflem1  8442  alephfp  8787  dfac5  8807  cardcf  8930  cfeq0  8934  sornom  8955  fpwwe2cbv  9304  fpwwe2lem3  9307  ltsosr  9767  map2psrpr  9783  axpre-lttri  9838  subval  10119  divval  10532  nn0ind-raph  11305  uzrdgfni  12570  sqeqor  12791  nn0opth2  12872  hashrabsn1  12972  elprchashprn2  12993  hashbclem  13041  hashbc  13042  hash2prde  13057  hash2pwpr  13061  brfi1indALT  13079  brfi1indALTOLD  13085  wrdind  13270  wrd2ind  13271  reuccats1lem  13273  cshf1  13349  wrdl3s3  13495  relexpindlem  13593  sqrtval  13767  sqrmo  13782  summolem2  14236  prodmolem2  14446  divides  14765  dvdstr  14798  odd2np1lem  14844  ndvdssub  14913  bitsinv1  14944  eucalglt  15078  hashgcdeq  15274  ramcl2lem  15493  ramcl  15513  cshwrepswhash1  15589  imasaddfnlem  15953  fnhomeqhomf  16116  initoeu2lem1  16429  posi  16715  sgrp2nmndlem3  17177  dfgrp2  17212  grpidinv  17240  dfgrp3lem  17278  orbsta  17511  symgfvne  17573  symgfix2  17601  odlem1  17719  gexlem1  17759  slwispgp  17791  sylow3lem6  17812  efgrelexlemb  17928  gsumval3lem2  18072  pgpfac1  18244  pgpfaclem2  18246  pgpfac  18248  ablfaclem1  18249  isdomn  19057  mvrval  19184  coe1tmmul2  19409  coe1tmmul  19410  obsip  19822  uvcval  19881  mat1comp  20003  mat1dimid  20037  scmateALT  20075  marrepval  20125  marepvval  20130  minmar1val  20211  gsummatr01  20222  t0sep  20876  t1sep2  20921  is2ndc  20997  kqt0lem  21287  isr0  21288  isufil2  21460  xmeteq0  21890  imasf1oxmet  21927  xrsxmet  22348  iccpnfcnv  22478  dyadmax  23085  dyadmbl  23087  dvfsumle  23501  dvfsumabs  23503  dvfsumlem1  23506  mdegle0  23554  fta1g  23644  ig1peu  23648  fta1  23780  aalioulem2  23805  efopn  24117  efrlim  24409  musum  24630  dvdsmulf1o  24633  dchrsum2  24706  sumdchr2  24708  gausslemma2dlem0i  24802  axtgcgrid  25075  axtgbtwnid  25078  tglowdim1i  25109  islmib  25393  axcontlem12  25569  wlkon  25823  wlkntrllem3  25853  spthonepeq  25879  fargshiftf1  25927  constr3trllem2  25941  wlklniswwlkn2  25990  usg2wlkeq  25998  wwlknredwwlkn  26016  wwlkextprop  26034  clwwlkn  26057  clwlkisclwwlklem2a4  26074  clwwlkext2edg  26092  clwwnisshclwwn  26099  hashecclwwlkn1  26123  usghashecclwwlk  26124  clwlkfoclwwlk  26134  2wlkonot  26154  2spthonot  26155  el2wlkonot  26158  el2spthonot  26159  el2spthonot0  26160  rusgraprop2  26231  rusgrasn  26234  rusgranumwlklem1  26238  rusgranumwlklem2  26239  rusgranumwlklem3  26240  rusgranumwlkg  26247  clwlknclwlkdifs  26249  frgra3vlem1  26289  3vfriswmgralem  26293  usg2spot2nb  26354  usgreg2spot  26356  2spotmdisj  26357  usgreghash2spot  26358  numclwwlkun  26368  numclwwlkdisj  26369  numclwwlkovf  26370  numclwwlkovg  26376  numclwlk1lem2f1  26383  numclwwlkovq  26388  numclwwlkovh  26390  numclwwlk5  26401  frgrareg  26406  frgraregord013  26407  friendshipgt3  26410  ex-opab  26443  isgrpoi  26498  grpoidinv2  26515  hvsubeq0  27111  hvaddcan  27113  hvsubadd  27120  normsub0  27179  omlsi  27449  pjoml  27481  nonbooli  27696  pj11  27759  lnopeq  28054  nmopun  28059  pjclem4a  28243  pj3lem1  28251  strlem4  28299  hstrlem4  28307  jplem1  28313  superpos  28399  rmoeqALT  28513  ifeqeqx  28547  disji2f  28574  disjif2  28578  disjabrex  28579  disjabrexf  28580  disjxpin  28585  disjunsn  28591  ofpreima  28650  fgreu  28656  fcnvgreu  28657  xrge0iifcnv  29109  esumpr2  29258  eulerpartlemgvv  29567  eulerpartlemgh  29569  eulerpartlemgs2  29571  sgnsub  29735  plymulx0  29752  bnj1321  30151  subfacp1lem3  30220  pconcn  30262  cnpcon  30268  txpcon  30270  conpcon  30273  cvmlift3lem2  30358  cvmlift3lem4  30360  cvmlift3  30366  snmlflim  30370  iota5f  30663  br1steqg  30721  br2ndeqg  30722  sltres  30863  nofulllem5  30907  rankeq1o  31250  nn0prpw  31290  bj-csbsnlem  31889  bj-restsnss  32016  bj-restsnss2  32017  fin2so  32365  poimirlem2  32380  poimirlem18  32396  poimirlem21  32399  poimirlem25  32403  poimirlem26  32404  poimirlem27  32405  mblfinlem2  32416  mbfresfi  32425  cnambfre  32427  ftc1anclem8  32461  f1opr  32488  fdc  32510  istotbnd  32537  isexid2  32623  isgrpda  32723  ismaxidl  32808  mpt2bi123f  32940  mptbi12f  32944  lsatcmp  33107  lshpkrlem1  33214  trlval2  34267  cdlemg1cex  34693  cdlemm10N  35224  dicval  35282  unxpwdom3  36482  dgraalem  36533  dgraaub  36536  frege104  37080  pm13.192  37432  2sbc6g  37437  2sbc5g  37438  pm14.122b  37445  equncomVD  37925  csbingVD  37941  csbsngVD  37950  csbxpgVD  37951  csbresgVD  37952  csbrngVD  37953  csbima12gALTVD  37954  csbunigVD  37955  csbfv12gALTVD  37956  relopabVD  37958  dvnprodlem1  38636  dvnprodlem2  38637  dvnprodlem3  38638  dvnprod  38639  fourierdlem42  38842  etransclem11  38938  etransclem12  38939  etransclem33  38960  nnfoctbdjlem  39148  hoimbl  39321  reuccatpfxs1lem  40097  clel5  40104  funsndifnop  40144  fundmge2nop0  40148  fpropnf1  40160  upgredgpr  40372  ushgredgedga  40454  ushgredgedgaloop  40456  rusgrpropnb  40781  rgrx0ndm  40791  uspgr2wlkeq  40852  wlkson  40862  upgrwlkdvdelem  40940  spthonepeq-av  40956  iswwlksnon  41049  1wlklnwwlkln2lem  41077  wwlksnredwwlkn  41099  wwlksnextprop  41116  wwlksnwwlksnon  41119  wwlks2onv  41156  elwwlks2ons3  41157  rusgrnumwwlklem  41171  clwwlknclwwlkdifs  41179  clwwlksn  41187  clwlkclwwlklem2a4  41204  clwwlksext2edg  41228  hashecclwwlksn1  41259  umgrhashecclwwlk  41260  clwlksfoclwwlk  41268  clwwlksndisj  41278  uhgr3cyclexlem  41346  1conngr  41359  frgr3vlem1  41441  3vfriswmgrlem  41445  frgr2wwlkeqm  41494  fusgr2wsp2nb  41496  fusgreg2wsp  41498  2wspmdisj  41499  fusgreghash2wsp  41500  av-numclwwlkovf  41509  av-numclwwlkovg  41516  av-numclwlk1lem2f1  41522  av-numclwwlkovq  41527  av-numclwwlkovh  41529  av-numclwwlk2lem1  41530  av-numclwwlk5  41540  av-frgraregord013  41547  av-friendshipgt3  41550  lidldomn1  41709  nn0sumshdiglem2  42212
  Copyright terms: Public domain W3C validator