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

Theorem eqeq2 2631
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 2630 1 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613
This theorem is referenced by:  eqeq2i  2632  eqeq12  2633  alexeqg  3326  clel5  3337  pm13.183  3338  eqeu  3371  moeq3  3377  mo2icl  3379  mob2  3380  euind  3387  reu6i  3391  reu2eqd  3397  reuind  3405  sbc2or  3438  sbc5  3454  csbiebg  3549  eqif  4117  sneq  4178  preq1b  4368  preqr1OLD  4371  prel12  4374  preq12bg  4377  prel12g  4378  preqsn  4384  disji2  4627  disjprg  4639  dtruALT  4890  dtruALT2  4902  opth  4935  euotd  4965  solin  5048  ideqg  5262  resieq  5395  cnveqb  5578  cnveq0  5579  iota5  5859  funopg  5910  fneq2  5968  foeq3  6100  tz6.12f  6199  funbrfv  6221  fnbrfvb  6223  fvelimab  6240  elrnrexdm  6349  funsndifnop  6401  fconst5  6456  eufnfv  6476  f1veqaeq  6499  fpropnf1  6509  isosolem  6582  mpt2eq123  6699  ovmpt4g  6768  ov3  6782  ovg  6784  caovcang  6820  caovcan  6823  tfisi  7043  tfindsg  7045  findsg  7078  f1oweALT  7137  seqomlem2  7531  oawordeu  7620  omopth  7723  ereq2  7735  qsdisj  7809  eroveu  7827  2dom  8014  fundmen  8015  xpf1o  8107  nneneq  8128  cantnflem1  8571  alephfp  8916  dfac5  8936  cardcf  9059  cfeq0  9063  sornom  9084  fpwwe2cbv  9437  fpwwe2lem3  9440  ltsosr  9900  map2psrpr  9916  axpre-lttri  9971  subval  10257  divval  10672  nn0ind-raph  11462  uzrdgfni  12740  sqeqor  12961  nn0opth2  13042  hashrabsn1  13146  elprchashprn2  13167  hashbclem  13219  hashbc  13220  hash2prde  13235  hash2pwpr  13241  brfi1indALT  13265  brfi1indALTOLD  13271  wrdind  13458  wrd2ind  13459  reuccats1lem  13461  cshf1  13537  wrdl3s3  13686  relexpindlem  13784  sqrtval  13958  sqrmo  13973  summolem2  14428  prodmolem2  14646  divides  14966  dvdstr  14999  odd2np1lem  15045  ndvdssub  15114  bitsinv1  15145  eucalglt  15279  hashgcdeq  15475  ramcl2lem  15694  ramcl  15714  cshwrepswhash1  15790  imasaddfnlem  16169  fnhomeqhomf  16332  initoeu2lem1  16645  posi  16931  sgrp2nmndlem3  17393  dfgrp2  17428  grpidinv  17456  dfgrp3lem  17494  orbsta  17727  symgfvne  17789  symgfix2  17817  odlem1  17935  gexlem1  17975  slwispgp  18007  sylow3lem6  18028  efgrelexlemb  18144  gsumval3lem2  18288  pgpfac1  18460  pgpfaclem2  18462  pgpfac  18464  ablfaclem1  18465  isdomn  19275  mvrval  19402  coe1tmmul2  19627  coe1tmmul  19628  obsip  20046  uvcval  20105  mat1comp  20227  mat1dimid  20261  scmateALT  20299  marrepval  20349  marepvval  20354  minmar1val  20435  gsummatr01  20446  t0sep  21109  t1sep2  21154  is2ndc  21230  kqt0lem  21520  isr0  21521  isufil2  21693  xmeteq0  22124  imasf1oxmet  22161  xrsxmet  22593  iccpnfcnv  22724  dyadmax  23347  dyadmbl  23349  dvfsumle  23765  dvfsumabs  23767  dvfsumlem1  23770  mdegle0  23818  fta1g  23908  ig1peu  23912  fta1  24044  aalioulem2  24069  efopn  24385  efrlim  24677  musum  24898  dvdsmulf1o  24901  dchrsum2  24974  sumdchr2  24976  gausslemma2dlem0i  25070  axtgcgrid  25343  axtgbtwnid  25346  tglowdim1i  25377  islmib  25660  axcontlem12  25836  upgredgpr  26018  ushgredgedg  26102  ushgredgedgloop  26104  rusgrpropnb  26460  rgrx0ndm  26470  uspgr2wlkeq  26523  wlkson  26533  upgrwlkdvdelem  26613  spthonepeq  26629  iswwlksnon  26721  wlklnwwlkln2lem  26749  wwlksnredwwlkn  26771  wwlksnextprop  26788  wwlksnwwlksnon  26791  wwlks2onv  26828  elwwlks2ons3  26829  rusgrnumwwlklem  26846  clwwlknclwwlkdifs  26854  clwwlksn  26862  clwlkclwwlklem2a4  26879  clwwlksext2edg  26903  hashecclwwlksn1  26934  umgrhashecclwwlk  26935  clwlksfoclwwlk  26943  clwwlksndisj  26953  uhgr3cyclexlem  27021  1conngr  27034  frgr3vlem1  27117  3vfriswmgrlem  27121  frgrwopreglem3  27156  fusgreg2wsplem  27171  fusgreghash2wsp  27176  numclwwlkovf  27185  numclwwlkovg  27192  numclwlk1lem2f1  27198  numclwwlkovq  27203  numclwwlkovh  27205  numclwwlk2lem1  27206  numclwwlk5  27216  frgrregord013  27223  friendshipgt3  27226  ex-opab  27259  isgrpoi  27322  grpoidinv2  27339  hvsubeq0  27895  hvaddcan  27897  hvsubadd  27904  normsub0  27963  omlsi  28233  pjoml  28265  nonbooli  28480  pj11  28543  lnopeq  28838  nmopun  28843  pjclem4a  29027  pj3lem1  29035  strlem4  29083  hstrlem4  29091  jplem1  29097  superpos  29183  rmoeqALT  29299  ifeqeqx  29333  disji2f  29362  disjif2  29366  disjabrex  29367  disjabrexf  29368  disjxpin  29373  disjunsn  29379  ofpreima  29439  fgreu  29445  fcnvgreu  29446  xrge0iifcnv  29953  esumpr2  30103  eulerpartlemgvv  30412  eulerpartlemgh  30414  eulerpartlemgs2  30416  sgnsub  30580  plymulx0  30598  bnj1321  31069  subfacp1lem3  31138  pconncn  31180  cnpconn  31186  txpconn  31188  connpconn  31191  cvmlift3lem2  31276  cvmlift3lem4  31278  cvmlift3  31284  snmlflim  31288  iota5f  31581  br1steqg  31648  br2ndeqg  31649  sltres  31789  noprefixmo  31822  nosupno  31823  nosupfv  31826  rankeq1o  32253  nn0prpw  32293  bj-csbsnlem  32873  bj-restsnss  33011  bj-restsnss2  33012  fin2so  33367  poimirlem2  33382  poimirlem18  33398  poimirlem21  33401  poimirlem25  33405  poimirlem26  33406  poimirlem27  33407  mblfinlem2  33418  mbfresfi  33427  cnambfre  33429  ftc1anclem8  33463  f1opr  33490  fdc  33512  istotbnd  33539  isexid2  33625  isgrpda  33725  ismaxidl  33810  mpt2bi123f  33942  mptbi12f  33946  lsatcmp  34109  lshpkrlem1  34216  trlval2  35269  cdlemg1cex  35695  cdlemm10N  36226  dicval  36284  unxpwdom3  37484  dgraalem  37534  dgraaub  37537  frege104  38081  pm13.192  38431  2sbc6g  38436  2sbc5g  38437  pm14.122b  38444  equncomVD  38924  csbingVD  38940  csbsngVD  38949  csbxpgVD  38950  csbresgVD  38951  csbrngVD  38952  csbima12gALTVD  38953  csbunigVD  38954  csbfv12gALTVD  38955  relopabVD  38957  dvnprodlem1  39924  dvnprodlem2  39925  dvnprodlem3  39926  dvnprod  39927  fourierdlem42  40129  etransclem11  40225  etransclem12  40226  etransclem33  40247  nnfoctbdjlem  40435  hoimbl  40608  fargshiftf1  41141  reuccatpfxs1lem  41198  uspgrsprf1  41520  uspgrsprfo  41521  lidldomn1  41686  nn0sumshdiglem2  42181  setrec2lem2  42206
  Copyright terms: Public domain W3C validator