Theorem eqeq2i 2744

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 2743	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 = 𝐴 ↔ 𝐶 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 = 𝐴 ↔ 𝐶 = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  eqeq12i  2749  eqtri  2759  neeq2i  3005  rabid2f  3436  rabid2OLD  3438  abv  3457  dfss2OLD  3934  equncom  4119  eq0  4308  ab0w  4338  ab0  4339  ab0OLD  4340  ab0orv  4343  eq0rdv  4369  rzal  4471  absn  4609  rabrsn  4690  ssunpr  4797  sspr  4798  sstp  4799  preq12b  4813  preqsnd  4821  preq12nebg  4825  opthprneg  4827  opeqpr  5467  propssopi  5470  wefrc  5632  dfrel4v  6147  dfrel4  6148  orddif  6418  funopg  6540  funimaexgOLD  6593  funcocnv2  6814  dffn5f  6918  fnressn  7109  fressnfv  7111  fnprb  7163  fntpb  7164  riotaeqimp  7345  fnov  7492  ovmpos  7508  onuninsuci  7781  fvresex  7897  elxp6  7960  el2xptp  7972  el2xptp0  7973  opiota  7996  tpossym  8194  dfwrecsOLD  8249  qsid  8729  mapsncnv  8838  ixpsnf1o  8883  card1  9913  pm54.43lem  9945  cf0  10196  sdom2en01  10247  cardeq0  10497  enqbreq2  10865  addcompr  10966  mulcompr  10968  axrrecex  11108  negeq0  11464  muleqadd  11808  crne0  12155  dfnn3  12176  xmulneg1  13198  hasheq0  14273  hashbc  14362  hashf1lem2  14367  hash2pwpr  14387  eqwrds3  14862  cjne0  15060  sqrt00  15160  sqrtmsq2i  15284  cbvsum  15591  fsump1i  15665  cbvprod  15809  bpoly2  15951  bpoly3  15952  bpoly4  15953  absefib  16091  efieq1re  16092  xpccatid  18090  sgrpidmnd  18575  smndex2dnrinv  18739  isnsg4  18983  selvval  21565  mat1dimelbas  21857  pmatcollpw3fi1lem1  22172  2ndcctbss  22843  ptcnp  23010  ovolgelb  24881  ioorinv  24977  rolle  25391  plymul0or  25678  reeff1o  25843  sineq0  25917  coseq1  25918  1cubr  26229  atandm2  26264  atandm3  26265  efrlim  26356  isppw  26500  ppiub  26589  lgsdinn0  26730  m1lgs  26773  uhgr2edg  28219  usgredg2vlem1  28236  usgredg2vlem2  28237  ushgredgedg  28240  ushgredgedgloop  28242  edgnbusgreu  28378  nb3grprlem2  28392  nb3gr2nb  28395  usgredgsscusgredg  28470  usgr2wlkneq  28767  usgr2pthlem  28774  crctcshwlkn0  28829  wwlksn0s  28869  umgr2adedgwlk  28953  umgr2adedgspth  28956  elwwlks2s3  28959  elwwlks2ons3im  28962  rusgrnumwwlkl1  28976  clwlkclwwlkflem  29011  isfrgr  29267  frgr3v  29282  frgrregorufr0  29331  isgrpo  29502  vciOLD  29566  chnlei  30490  h1de2ctlem  30560  cmcmlem  30596  cmcm2i  30598  cmbr2i  30601  osumcor2i  30649  pjss2i  30685  ho01i  30833  nmop0h  30996  pjclem1  31200  jplem1  31273  atabs2i  31407  fedgmullem2  32412  ccfldextdgrr  32443  zarcls  32544  breprexp  33335  bnj168  33431  bnj927  33470  bnj543  33594  bnj970  33648  subfacp1lem6  33866  satfv1  34044  satfvsucsuc  34046  satf0  34053  fmlaomn0  34071  fmla0disjsuc  34079  satffunlem2lem1  34085  mppspstlem  34252  quad3  34345  brdomain  34594  brrange  34595  brimg  34598  brapply  34599  brsuccf  34602  brfullfun  34609  brrestrict  34610  rankeq1o  34832  bj-snsetex  35507  bj-reabeq  35571  bj-rest10  35632  bj-ismooredr2  35654  bj-pinftynminfty  35771  dffinxpf  35929  finxp0  35935  matunitlindflem1  36147  ismblfin  36192  opropabco  36256  fdc  36277  isdrngo1  36488  smprngopr  36584  eldisjlem19  37345  cdleme25cv  38894  cdlemk35  39448  dicval2  39715  dicopelval2  39717  dicelval2N  39718  hdmap1fval  40332  sn-0tie0  40966  mzpcompact2lem  41132  eldioph4b  41192  2nn0ind  41327  islmodfg  41454  abeqabi  41802  relintab  41977  brtrclfv2  42121  frege116  42373  elnev  42840  dvnprodlem1  44307  fourierdlem103  44570  fourierdlem104  44571  ovnovollem3  45019  fmtno4prmfac  45884  lindsrng01  46669  ldepspr  46674  nn0sumshdiglemB  46826  mofeu  47034