Theorem eqeq2i 2622

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

Syntax hints:   ↔ wb 195   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  eqeq12i  2624  eqtri  2632  neeq2i  2847  rabid2  3096  dfss2  3557  equncom  3720  rabrsn  4203  ssunpr  4305  sspr  4306  sstp  4307  preq12b  4322  preqsnd  4330  preqsn  4331  preqsnOLD  4332  opeqpr  4893  propssopi  4896  wefrc  5032  dfrel4v  5503  dfrel4  5504  orddif  5737  dfiota2  5769  funopg  5836  funimaexg  5889  funcocnv2  6074  dffn5f  6162  fnressn  6330  fressnfv  6332  fnprb  6377  fntpb  6378  fnov  6666  ovmpt2s  6682  onuninsuci  6932  fvresex  7032  elxp6  7091  el2xptp  7102  el2xptp0  7103  opiota  7118  tpossym  7271  qsid  7700  mapsncnv  7790  ixpsnf1o  7834  card1  8677  pm54.43lem  8708  cf0  8956  sdom2en01  9007  cardeq0  9253  enqbreq2  9621  addcompr  9722  mulcompr  9724  axrrecex  9863  negeq0  10214  muleqadd  10550  crne0  10890  dfnn3  10911  xmulneg1  11971  hasheq0  13015  hashbc  13094  hashf1lem2  13097  hash2pwpr  13115  eqwrds3  13552  cjne0  13751  sqrt00  13852  sqrtmsq2i  13975  cbvsum  14273  fsump1i  14342  cbvprod  14484  bpoly2  14627  bpoly3  14628  bpoly4  14629  absefib  14767  efieq1re  14768  xpccatid  16651  isnsg4  17460  mat1dimelbas  20096  pmatcollpw3fi1lem1  20410  2ndcctbss  21068  ptcnp  21235  ovolgelb  23055  ioorinv  23150  rolle  23557  plymul0or  23840  reeff1o  24005  sineq0  24077  coseq1  24078  1cubr  24369  atandm2  24404  atandm3  24405  efrlim  24496  isppw  24640  ppiub  24729  lgsdinn0  24870  m1lgs  24913  usgra2edg  25911  usgraedg4  25916  usgraidx2vlem1  25920  usgraidx2vlem2  25921  nb3graprlem2  25981  nb3grapr  25982  nb3grapr2  25983  nb3gra2nb  25984  2trllemH  26082  2trllemE  26083  usgrcyclnl2  26169  4cycl4dv  26195  wwlkn0  26217  wwlkn0s  26233  rusgranumwlkl1  26474  2pthfrgra  26538  isgrpo  26735  vciOLD  26800  chnlei  27728  h1de2ctlem  27798  cmcmlem  27834  cmcm2i  27836  cmbr2i  27839  osumcor2i  27887  pjss2i  27923  ho01i  28071  nmop0h  28234  pjclem1  28438  jplem1  28511  atabs2i  28645  rabid2f  28724  bnj168  30052  bnj927  30093  bnj543  30217  bnj970  30271  subfacp1lem6  30421  mppspstlem  30722  quad3  30818  trpredmintr  30975  brdomain  31210  brrange  31211  brimg  31214  brapply  31215  brsuccf  31218  brfullfun  31225  brrestrict  31226  rankeq1o  31448  bj-snsetex  32144  bj-rest10  32222  bj-pinftynminfty  32291  dffinxpf  32398  finxp0  32404  matunitlindflem1  32575  ismblfin  32620  opropabco  32688  fdc  32711  isdrngo1  32925  smprngopr  33021  cdleme25cv  34664  cdlemk35  35218  dicval2  35486  dicopelval2  35488  dicelval2N  35489  hdmap1fval  36104  mzpcompact2lem  36332  eldioph4b  36393  2nn0ind  36528  islmodfg  36657  relintab  36908  brtrclfv2  37038  frege116  37293  elnev  37661  dvnprodlem1  38836  fourierdlem103  39102  fourierdlem104  39103  ovnovollem3  39548  fmtno4prmfac  40022  riotaeqimp  40338  uhgr2edg  40435  usgredg2vlem1  40452  usgredg2vlem2  40453  ushgredgedga  40456  ushgredgedgaloop  40458  edgnbusgreu  40595  nb3grprlem2  40609  nb3gr2nb  40612  usgredgsscusgredg  40675  usgr2wlkneq  40962  usgr2pthlem  40969  crctcsh1wlkn0  41024  wwlksn0s  41057  umgr2adedgwlk  41152  umgr2adedgspth  41155  elwwlks2ons3  41159  elwwlks2s3  41169  rusgrnumwwlkl1  41172  frgr3v  41445  lindsrng01  42051  ldepspr  42056  nn0sumshdiglemB  42212