Theorem eqeq2i 2742

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeq12i  2747  eqtri  2752  neeq2i  2990  rabid2f  3434  rabid2im  3435  abv  3456  equncom  4118  eq0  4309  ab0w  4338  ab0  4339  ab0orv  4342  eq0rdv  4366  rzal  4468  absn  4605  rabrsn  4684  ssunpr  4794  sspr  4795  sstp  4796  preq12b  4810  preqsnd  4819  preq12nebg  4823  opthprneg  4825  opeqpr  5460  propssopi  5463  wefrc  5625  dfrel4v  6151  dfrel4  6152  orddif  6418  funopg  6534  f1imadifssran  6586  funcocnv2  6807  dffn5f  6914  fnressn  7112  fressnfv  7114  fnprb  7164  fntpb  7165  riotaeqimp  7352  fnov  7500  ovmpos  7517  onuninsuci  7796  fvresex  7918  elxp6  7981  el2xptp  7993  el2xptp0  7994  opiota  8017  tpossym  8214  qsid  8731  mapsncnv  8843  ixpsnf1o  8888  card1  9897  pm54.43lem  9929  cf0  10180  sdom2en01  10231  cardeq0  10481  enqbreq2  10849  addcompr  10950  mulcompr  10952  axrrecex  11092  negeq0  11452  muleqadd  11798  crne0  12155  dfnn3  12176  xmulneg1  13205  hasheq0  14304  hashbc  14394  hashf1lem2  14397  hash2pwpr  14417  eqwrds3  14903  cjne0  15105  sqrt00  15205  sqrtmsq2i  15330  cbvsum  15637  cbvsumv  15638  fsump1i  15711  cbvprod  15855  cbvprodv  15856  bpoly2  15999  bpoly3  16000  bpoly4  16001  absefib  16142  efieq1re  16143  xpccatid  18129  sgrpidmnd  18648  smndex2dnrinv  18824  isnsg4  19081  opprdomnb  20637  selvval  22055  mat1dimelbas  22391  pmatcollpw3fi1lem1  22706  2ndcctbss  23375  ptcnp  23542  ovolgelb  25414  ioorinv  25510  dvcobr  25882  rolle  25927  dvfsumlem2  25966  plymul0or  26221  reeff1o  26390  sineq0  26466  coseq1  26467  1cubr  26785  atandm2  26820  atandm3  26821  efrlim  26912  efrlimOLD  26913  isppw  27057  ppiub  27148  lgsdinn0  27289  m1lgs  27332  elzs2  28327  elznns  28330  1p1e2s  28343  twocut  28350  uhgr2edg  29188  usgredg2vlem1  29205  usgredg2vlem2  29206  ushgredgedg  29209  ushgredgedgloop  29211  edgnbusgreu  29347  nb3grprlem2  29361  nb3gr2nb  29364  usgredgsscusgredg  29440  usgr2wlkneq  29736  usgr2pthlem  29743  crctcshwlkn0  29801  wwlksn0s  29841  umgr2adedgwlk  29925  umgr2adedgspth  29928  elwwlks2s3  29931  elwwlks2ons3im  29934  rusgrnumwwlkl1  29948  clwlkclwwlkflem  29983  isfrgr  30239  frgr3v  30254  frgrregorufr0  30303  isgrpo  30476  vciOLD  30540  chnlei  31464  h1de2ctlem  31534  cmcmlem  31570  cmcm2i  31572  cmbr2i  31575  osumcor2i  31623  pjss2i  31659  ho01i  31807  nmop0h  31970  pjclem1  32174  jplem1  32247  atabs2i  32381  1arithidom  33501  ply1dg1rt  33541  fedgmullem2  33619  ccfldextdgrr  33660  zarcls  33857  breprexp  34617  bnj168  34713  bnj927  34752  bnj543  34876  bnj970  34930  subfacp1lem6  35165  satfv1  35343  satfvsucsuc  35345  satf0  35352  fmlaomn0  35370  fmla0disjsuc  35378  satffunlem2lem1  35384  mppspstlem  35551  quad3  35650  brdomain  35914  brrange  35915  brimg  35918  brapply  35919  brsuccf  35922  brfullfun  35929  brrestrict  35930  rankeq1o  36152  sumeq2si  36183  prodeq2si  36185  cbvprodvw2  36228  bj-snsetex  36944  bj-reabeq  37008  bj-rest10  37069  bj-ismooredr2  37091  bj-pinftynminfty  37208  dffinxpf  37366  finxp0  37372  matunitlindflem1  37603  ismblfin  37648  opropabco  37711  fdc  37732  isdrngo1  37943  smprngopr  38039  qseq  38633  eldisjlem19  38795  cdleme25cv  40345  cdlemk35  40899  dicval2  41166  dicopelval2  41168  dicelval2N  41169  hdmap1fval  41783  sn-0tie0  42432  absnw  42659  mzpcompact2lem  42732  eldioph4b  42792  2nn0ind  42927  islmodfg  43051  abeqabi  43390  relintab  43565  brtrclfv2  43709  frege116  43961  elnev  44420  dvnprodlem1  45937  fourierdlem103  46200  fourierdlem104  46201  ovnovollem3  46649  fmtno4prmfac  47566  usgrexmpl2nb1  48016  usgrexmpl2nb2  48017  usgrexmpl2nb3  48018  usgrexmpl2nb4  48019  usgrexmpl2nb5  48020  pgnioedg1  48091  pgnioedg2  48092  pgnioedg3  48093  pgnioedg4  48094  pgnioedg5  48095  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  pgnbgreunbgrlem5lem1  48103  pgnbgreunbgrlem5lem2  48104  pgnbgreunbgrlem5lem3  48105  lindsrng01  48450  ldepspr  48455  nn0sumshdiglemB  48602  mofeu  48829  f1omo  48874