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

Theorem eqeq2 2833
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 2832 1 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  eqeq2i  2834  eqeq12  2835  alexeqg  3643  clel5OLD  3657  pm13.183  3658  pm13.183OLD  3659  eqeu  3696  moeq3  3702  mo2icl  3704  mob2  3705  euind  3714  reu6i  3718  reu2eqd  3726  reuind  3743  sbc2or  3780  sbc5  3799  csbiebg  3914  eqif  4505  sneq  4569  reusngf  4606  rexreusng  4611  reuprg0  4632  preq1b  4771  preq12bg  4778  preqsn  4786  disji2  5040  disjprgw  5053  disjprg  5054  dtruALT  5280  dtruALT2  5327  opth  5360  euotd  5395  solin  5492  ideqg  5716  resieq  5858  cnveqb  6047  cnveq0  6048  reu3op  6137  reuop  6138  iota5  6332  funopg  6383  fneq2  6439  foeq3  6582  tz6.12f  6688  funbrfv  6710  fnbrfvb  6712  fvelimab  6731  elrnrexdm  6848  funsndifnop  6906  fconst5  6961  eufnfv  6983  f1veqaeq  7006  fpropnf1  7016  isosolem  7089  f1opr  7199  mpoeq123  7215  ovmpt4g  7286  ov3  7300  ovg  7302  caovcang  7338  caovcan  7341  tfisi  7561  tfindsg  7563  findsg  7597  f1oweALT  7664  seqomlem2  8078  oawordeu  8171  omopth  8275  ereq2  8287  qsdisj  8364  eroveu  8382  2dom  8571  fundmen  8572  xpf1o  8668  nneneq  8689  cantnflem1  9141  updjud  9352  alephfp  9523  dfac5  9543  cardcf  9663  cfeq0  9667  sornom  9688  fpwwe2cbv  10041  fpwwe2lem3  10044  ltsosr  10505  map2psrpr  10521  axpre-lttri  10576  subval  10866  divval  11289  nn0ind-raph  12071  uzrdgfni  13316  sqeqor  13568  nn0opth2  13622  hashrabsn1  13725  elprchashprn2  13747  hashbclem  13800  hashbc  13801  hash2prde  13818  hash2pwpr  13824  brfi1indALT  13848  wrdind  14074  wrd2ind  14075  reuccatpfxs1lem  14098  cshf1  14162  wrdl3s3  14316  relexpindlem  14412  sqrtval  14586  sqrmo  14601  reusq0  14812  summolem2  15063  prodmolem2  15279  divides  15599  dvdstr  15636  odd2np1lem  15679  ndvdssub  15750  bitsinv1  15781  eucalglt  15919  hashgcdeq  16116  ramcl2lem  16335  ramcl  16355  cshwrepswhash1  16426  imasaddfnlem  16791  fnhomeqhomf  16951  initoeu2lem1  17264  posi  17550  sgrp2nmndlem3  18030  dfgrp2  18068  grpidinv  18099  dfgrp3lem  18137  orbsta  18383  symgfvne  18446  symgfix2  18475  odlem1  18594  gexlem1  18635  slwispgp  18667  sylow3lem6  18688  efgrelexlemb  18807  gsumval3lem2  18957  pgpfac1  19133  pgpfaclem2  19135  pgpfac  19137  ablfaclem1  19138  isdomn  19997  mvrval  20131  mhpval  20263  coe1tmmul2  20374  coe1tmmul  20375  obsip  20795  uvcval  20859  mat1comp  20979  mat1dimid  21013  scmateALT  21051  marrepval  21101  marepvval  21106  minmar1val  21187  gsummatr01  21198  t0sep  21862  t1sep2  21907  is2ndc  21984  kqt0lem  22274  isr0  22275  isufil2  22446  xmeteq0  22877  imasf1oxmet  22914  xrsxmet  23346  iccpnfcnv  23477  dyadmax  24128  dyadmbl  24130  dvfsumle  24547  dvfsumabs  24549  dvfsumlem1  24552  mdegle0  24600  fta1g  24690  ig1peu  24694  fta1  24826  aalioulem2  24851  efopn  25168  efrlim  25475  musum  25696  dvdsmulf1o  25699  dchrsum2  25772  sumdchr2  25774  gausslemma2dlem0i  25868  addsqnreup  25947  2sqreulem1  25950  2sqreultblem  25952  2sqreunnlem1  25953  2sqreunnltblem  25955  2sqreulem3  25957  axtgcgrid  26177  axtgbtwnid  26180  tglowdim1i  26215  islmib  26501  axcontlem12  26689  upgredgpr  26855  ushgredgedg  26939  ushgredgedgloop  26941  rusgrpropnb  27293  rgrx0ndm  27303  uspgr2wlkeq  27355  wlkson  27366  upgrwlkdvdelem  27445  spthonepeq  27461  iswwlksnon  27559  wlklnwwlkln2lem  27588  wwlksnredwwlkn  27601  wwlksnextprop  27619  wwlksnwwlksnon  27622  elwwlks2ons3  27662  rusgrnumwwlklem  27677  clwlkclwwlklem2a4  27703  clwwlkn  27732  clwwlkext2edg  27763  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwwlknon  27797  clwwlk0on0  27799  uhgr3cyclexlem  27888  1conngr  27901  frgr3vlem1  27980  3vfriswmgrlem  27984  frgrwopreglem3  28021  fusgreg2wsplem  28040  fusgreghash2wsp  28045  numclwlk1lem1  28076  numclwwlkovq  28081  numclwwlk2lem1  28083  frgrregord013  28102  friendshipgt3  28105  ex-opab  28139  isgrpoi  28203  grpoidinv2  28220  hvsubeq0  28773  hvaddcan  28775  hvsubadd  28782  normsub0  28841  omlsi  29109  pjoml  29141  nonbooli  29356  pj11  29419  lnopeq  29714  nmopun  29719  pjclem4a  29903  pj3lem1  29911  strlem4  29959  hstrlem4  29967  jplem1  29973  superpos  30059  ifeqeqx  30225  disji2f  30256  disjif2  30260  disjabrex  30261  disjabrexf  30262  disjxpin  30267  disjunsn  30273  ofpreima  30339  fgreu  30346  fcnvgreu  30347  xrge0iifcnv  31076  esumpr2  31226  eulerpartlemgvv  31534  eulerpartlemgh  31536  eulerpartlemgs2  31538  sgnsub  31702  plymulx0  31717  lpadmax  31853  lpadright  31855  bnj1321  32197  f1resfz0f1d  32259  subfacp1lem3  32327  pconncn  32369  cnpconn  32375  txpconn  32377  connpconn  32380  cvmlift3lem2  32465  cvmlift3lem4  32467  cvmlift3  32473  snmlflim  32477  iota5f  32853  sltres  33067  noprefixmo  33100  nosupno  33101  nosupfv  33104  rankeq1o  33530  nn0prpw  33569  bj-csbsnlem  34118  bj-restsnss  34269  bj-restsnss2  34270  fin2so  34761  poimirlem2  34776  poimirlem18  34792  poimirlem21  34795  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  mblfinlem2  34812  mbfresfi  34820  cnambfre  34822  ftc1anclem8  34856  fdc  34903  istotbnd  34930  isexid2  35016  isgrpda  35116  ismaxidl  35201  mpobi123f  35323  mptbi12f  35327  qsdisjALTV  35732  lsatcmp  36021  lshpkrlem1  36128  trlval2  37181  cdlemg1cex  37606  cdlemm10N  38136  dicval  38194  nnn1suc  39039  resubval  39077  unxpwdom3  39575  dgraalem  39625  dgraaub  39628  frege104  40193  pm13.192  40622  2sbc6g  40627  2sbc5g  40628  pm14.122b  40635  equncomVD  41082  csbingVD  41098  csbsngVD  41107  csbxpgVD  41108  csbresgVD  41109  csbrngVD  41110  csbima12gALTVD  41111  csbunigVD  41112  csbfv12gALTVD  41113  relopabVD  41115  dvnprodlem1  42111  dvnprodlem2  42112  dvnprodlem3  42113  dvnprod  42114  fourierdlem42  42315  etransclem11  42411  etransclem12  42412  etransclem33  42433  nnfoctbdjlem  42618  hoimbl  42794  aiota0def  43175  euoreqb  43189  funressndmafv2rn  43303  funressnbrafv2  43324  dfatbrafv2b  43325  funbrafv2  43327  fnbrafv2b  43328  fargshiftf1  43448  ichnreuop  43481  paireqne  43520  reupr  43531  uspgrsprf1  43869  uspgrsprfo  43870  lidldomn1  44090  nn0sumshdiglem2  44580  setrec2lem2  44695
  Copyright terms: Public domain W3C validator