Theorem eqeq2i 2790

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq2i	⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq2 2789	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Syntax hints:   ↔ wb 198   = wceq 1507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2771

This theorem is referenced by:  eqeq12i  2792  eqtri  2802  neeq2i  3032  rabid2  3320  rabid2f  3321  dfss2  3846  equncom  4019  absn  4459  rabrsn  4534  ssunpr  4639  sspr  4640  sstp  4641  preq12b  4655  preqsnd  4663  preq12nebg  4667  opthprneg  4669  opeqpr  5251  propssopi  5254  wefrc  5401  dfrel4v  5887  dfrel4  5888  orddif  6122  funopg  6222  funimaexg  6273  funcocnv2  6468  dffn5f  6565  fnressn  6743  fressnfv  6745  fnprb  6797  fntpb  6798  riotaeqimp  6960  fnov  7098  ovmpos  7114  onuninsuci  7371  fvresex  7473  elxp6  7535  el2xptp  7547  el2xptp0  7548  opiota  7565  tpossym  7727  qsid  8163  mapsncnv  8255  ixpsnf1o  8299  card1  9191  pm54.43lem  9222  cf0  9471  sdom2en01  9522  cardeq0  9772  enqbreq2  10140  addcompr  10241  mulcompr  10243  axrrecex  10383  negeq0  10741  muleqadd  11085  crne0  11432  dfnn3  11455  xmulneg1  12478  hasheq0  13539  hashbc  13624  hashf1lem2  13627  hash2pwpr  13645  eqwrds3  14186  cjne0  14383  sqrt00  14484  sqrtmsq2i  14608  cbvsum  14912  fsump1i  14984  cbvprod  15129  bpoly2  15271  bpoly3  15272  bpoly4  15273  absefib  15411  efieq1re  15412  xpccatid  17296  isnsg4  18106  mat1dimelbas  20784  pmatcollpw3fi1lem1  21098  2ndcctbss  21767  ptcnp  21934  ovolgelb  23784  ioorinv  23880  rolle  24290  plymul0or  24573  reeff1o  24738  sineq0  24812  coseq1  24813  1cubr  25121  atandm2  25156  atandm3  25157  efrlim  25249  isppw  25393  ppiub  25482  lgsdinn0  25623  m1lgs  25666  uhgr2edg  26693  usgredg2vlem1  26710  usgredg2vlem2  26711  ushgredgedg  26714  ushgredgedgloop  26716  edgnbusgreu  26852  nb3grprlem2  26866  nb3gr2nb  26869  usgredgsscusgredg  26944  usgr2wlkneq  27245  usgr2pthlem  27252  crctcshwlkn0  27307  wwlksn0s  27347  umgr2adedgwlk  27451  umgr2adedgspth  27454  elwwlks2s3  27457  elwwlks2ons3im  27460  rusgrnumwwlkl1  27474  clwlkclwwlkflem  27512  frgr3v  27809  frgrregorufr0  27858  isgrpo  28051  vciOLD  28115  chnlei  29043  h1de2ctlem  29113  cmcmlem  29149  cmcm2i  29151  cmbr2i  29154  osumcor2i  29202  pjss2i  29238  ho01i  29386  nmop0h  29549  pjclem1  29753  jplem1  29826  atabs2i  29960  fedgmullem2  30661  ccfldextdgrr  30692  breprexp  31558  bnj168  31654  bnj927  31694  bnj543  31818  bnj970  31872  subfacp1lem6  32023  satf0  32188  mppspstlem  32344  quad3  32439  trpredmintr  32597  brdomain  32921  brrange  32922  brimg  32925  brapply  32926  brsuccf  32929  brfullfun  32936  brrestrict  32937  rankeq1o  33159  bj-snsetex  33799  bj-rest10  33895  bj-pinftynminfty  33984  dffinxpf  34113  finxp0  34119  matunitlindflem1  34335  ismblfin  34380  opropabco  34447  fdc  34468  isdrngo1  34682  smprngopr  34778  cdleme25cv  36945  cdlemk35  37499  dicval2  37766  dicopelval2  37768  dicelval2N  37769  hdmap1fval  38383  mzpcompact2lem  38749  eldioph4b  38810  2nn0ind  38944  islmodfg  39071  relintab  39311  brtrclfv2  39441  frege116  39694  elnev  40193  dvnprodlem1  41667  fourierdlem103  41931  fourierdlem104  41932  ovnovollem3  42377  fmtno4prmfac  43108  lindsrng01  43896  ldepspr  43901  nn0sumshdiglemB  44054