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

Theorem eqeq2 2830
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 2829 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 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  eqeq2i  2831  eqeq12  2832  alexeqg  3641  clel5OLD  3655  pm13.183  3656  pm13.183OLD  3657  eqeu  3694  moeq3  3700  mo2icl  3702  mob2  3703  euind  3712  reu6i  3716  reu2eqd  3724  reuind  3741  sbc2or  3778  sbc5  3797  csbiebg  3912  eqif  4503  sneq  4567  reusngf  4604  rexreusng  4609  reuprg0  4630  preq1b  4769  preq12bg  4776  preqsn  4784  disji2  5039  disjprgw  5052  disjprg  5053  dtruALT  5279  dtruALT2  5326  opth  5359  euotd  5394  solin  5491  ideqg  5715  resieq  5857  cnveqb  6046  cnveq0  6047  reu3op  6136  reuop  6137  iota5  6331  funopg  6382  fneq2  6438  foeq3  6581  tz6.12f  6687  funbrfv  6709  fnbrfvb  6711  fvelimab  6730  elrnrexdm  6847  funsndifnop  6905  fconst5  6960  eufnfv  6982  f1veqaeq  7006  fpropnf1  7016  isosolem  7089  f1opr  7199  mpoeq123  7215  ovmpt4g  7286  ov3  7300  ovg  7302  caovcang  7338  caovcan  7341  tfisi  7562  tfindsg  7564  findsg  7598  f1oweALT  7662  seqomlem2  8076  oawordeu  8170  omopth  8274  ereq2  8286  qsdisj  8363  eroveu  8381  2dom  8570  fundmen  8571  xpf1o  8667  nneneq  8688  cantnflem1  9140  updjud  9351  alephfp  9522  dfac5  9542  cardcf  9662  cfeq0  9666  sornom  9687  fpwwe2cbv  10040  fpwwe2lem3  10043  ltsosr  10504  map2psrpr  10520  axpre-lttri  10575  subval  10865  divval  11288  nn0ind-raph  12070  uzrdgfni  13314  sqeqor  13566  nn0opth2  13620  hashrabsn1  13723  elprchashprn2  13745  hashbclem  13798  hashbc  13799  hash2prde  13816  hash2pwpr  13822  brfi1indALT  13846  wrdind  14072  wrd2ind  14073  reuccatpfxs1lem  14096  cshf1  14160  wrdl3s3  14314  relexpindlem  14410  sqrtval  14584  sqrmo  14599  reusq0  14810  summolem2  15061  prodmolem2  15277  divides  15597  dvdstr  15634  odd2np1lem  15677  ndvdssub  15748  bitsinv1  15779  eucalglt  15917  hashgcdeq  16114  ramcl2lem  16333  ramcl  16353  cshwrepswhash1  16424  imasaddfnlem  16789  fnhomeqhomf  16949  initoeu2lem1  17262  posi  17548  sgrp2nmndlem3  18028  dfgrp2  18066  grpidinv  18097  dfgrp3lem  18135  orbsta  18381  symgfvne  18444  symgfix2  18473  odlem1  18592  gexlem1  18633  slwispgp  18665  sylow3lem6  18686  efgrelexlemb  18805  gsumval3lem2  18955  pgpfac1  19131  pgpfaclem2  19133  pgpfac  19135  ablfaclem1  19136  isdomn  19995  mvrval  20129  mhpval  20261  coe1tmmul2  20372  coe1tmmul  20373  obsip  20793  uvcval  20857  mat1comp  20977  mat1dimid  21011  scmateALT  21049  marrepval  21099  marepvval  21104  minmar1val  21185  gsummatr01  21196  t0sep  21860  t1sep2  21905  is2ndc  21982  kqt0lem  22272  isr0  22273  isufil2  22444  xmeteq0  22875  imasf1oxmet  22912  xrsxmet  23344  iccpnfcnv  23475  dyadmax  24126  dyadmbl  24128  dvfsumle  24545  dvfsumabs  24547  dvfsumlem1  24550  mdegle0  24598  fta1g  24688  ig1peu  24692  fta1  24824  aalioulem2  24849  efopn  25168  efrlim  25474  musum  25695  dvdsmulf1o  25698  dchrsum2  25771  sumdchr2  25773  gausslemma2dlem0i  25867  addsqnreup  25946  2sqreulem1  25949  2sqreultblem  25951  2sqreunnlem1  25952  2sqreunnltblem  25954  2sqreulem3  25956  axtgcgrid  26176  axtgbtwnid  26179  tglowdim1i  26214  islmib  26500  axcontlem12  26688  upgredgpr  26854  ushgredgedg  26938  ushgredgedgloop  26940  rusgrpropnb  27292  rgrx0ndm  27302  uspgr2wlkeq  27354  wlkson  27365  upgrwlkdvdelem  27444  spthonepeq  27460  iswwlksnon  27558  wlklnwwlkln2lem  27587  wwlksnredwwlkn  27600  wwlksnextprop  27618  wwlksnwwlksnon  27621  elwwlks2ons3  27661  rusgrnumwwlklem  27676  clwlkclwwlklem2a4  27702  clwwlkn  27731  clwwlkext2edg  27762  hashecclwwlkn1  27783  umgrhashecclwwlk  27784  clwwlknon  27796  clwwlk0on0  27798  uhgr3cyclexlem  27887  1conngr  27900  frgr3vlem1  27979  3vfriswmgrlem  27983  frgrwopreglem3  28020  fusgreg2wsplem  28039  fusgreghash2wsp  28044  numclwlk1lem1  28075  numclwwlkovq  28080  numclwwlk2lem1  28082  frgrregord013  28101  friendshipgt3  28104  ex-opab  28138  isgrpoi  28202  grpoidinv2  28219  hvsubeq0  28772  hvaddcan  28774  hvsubadd  28781  normsub0  28840  omlsi  29108  pjoml  29140  nonbooli  29355  pj11  29418  lnopeq  29713  nmopun  29718  pjclem4a  29902  pj3lem1  29910  strlem4  29958  hstrlem4  29966  jplem1  29972  superpos  30058  ifeqeqx  30224  disji2f  30255  disjif2  30259  disjabrex  30260  disjabrexf  30261  disjxpin  30266  disjunsn  30272  ofpreima  30338  fgreu  30345  fcnvgreu  30346  xrge0iifcnv  31075  esumpr2  31225  eulerpartlemgvv  31533  eulerpartlemgh  31535  eulerpartlemgs2  31537  sgnsub  31701  plymulx0  31716  lpadmax  31852  lpadright  31854  bnj1321  32196  f1resfz0f1d  32258  subfacp1lem3  32326  pconncn  32368  cnpconn  32374  txpconn  32376  connpconn  32379  cvmlift3lem2  32464  cvmlift3lem4  32466  cvmlift3  32472  snmlflim  32476  iota5f  32852  sltres  33066  noprefixmo  33099  nosupno  33100  nosupfv  33103  rankeq1o  33529  nn0prpw  33568  bj-csbsnlem  34117  bj-restsnss  34268  bj-restsnss2  34269  fin2so  34760  poimirlem2  34775  poimirlem18  34791  poimirlem21  34794  poimirlem25  34798  poimirlem26  34799  poimirlem27  34800  mblfinlem2  34811  mbfresfi  34819  cnambfre  34821  ftc1anclem8  34855  fdc  34901  istotbnd  34928  isexid2  35014  isgrpda  35114  ismaxidl  35199  mpobi123f  35321  mptbi12f  35325  qsdisjALTV  35730  lsatcmp  36019  lshpkrlem1  36126  trlval2  37179  cdlemg1cex  37604  cdlemm10N  38134  dicval  38192  nnn1suc  39037  resubval  39075  unxpwdom3  39573  dgraalem  39623  dgraaub  39626  frege104  40191  pm13.192  40619  2sbc6g  40624  2sbc5g  40625  pm14.122b  40632  equncomVD  41079  csbingVD  41095  csbsngVD  41104  csbxpgVD  41105  csbresgVD  41106  csbrngVD  41107  csbima12gALTVD  41108  csbunigVD  41109  csbfv12gALTVD  41110  relopabVD  41112  dvnprodlem1  42107  dvnprodlem2  42108  dvnprodlem3  42109  dvnprod  42110  fourierdlem42  42311  etransclem11  42407  etransclem12  42408  etransclem33  42429  nnfoctbdjlem  42614  hoimbl  42790  aiota0def  43171  euoreqb  43185  funressndmafv2rn  43299  funressnbrafv2  43320  dfatbrafv2b  43321  funbrafv2  43323  fnbrafv2b  43324  elsetpreimafvbi  43428  elsetpreimafveq  43434  imasetpreimafvbijlemfo  43442  fargshiftf1  43478  ichnreuop  43511  paireqne  43550  reupr  43561  uspgrsprf1  43899  uspgrsprfo  43900  lidldomn1  44120  nn0sumshdiglem2  44610  setrec2lem2  44725
  Copyright terms: Public domain W3C validator