Theorem eqeq2i 2743

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 2742	. 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 2702

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

This theorem is referenced by:  eqeq12i  2748  eqtri  2753  neeq2i  2991  rabid2f  3440  rabid2im  3441  abv  3462  equncom  4125  eq0  4316  ab0w  4345  ab0  4346  ab0orv  4349  eq0rdv  4373  rzal  4475  absn  4612  rabrsn  4691  ssunpr  4801  sspr  4802  sstp  4803  preq12b  4817  preqsnd  4826  preq12nebg  4830  opthprneg  4832  opeqpr  5468  propssopi  5471  wefrc  5635  dfrel4v  6166  dfrel4  6167  orddif  6433  funopg  6553  f1imadifssran  6605  funimaexgOLD  6607  funcocnv2  6828  dffn5f  6935  fnressn  7133  fressnfv  7135  fnprb  7185  fntpb  7186  riotaeqimp  7373  fnov  7523  ovmpos  7540  onuninsuci  7819  fvresex  7941  elxp6  8005  el2xptp  8017  el2xptp0  8018  opiota  8041  tpossym  8240  qsid  8757  mapsncnv  8869  ixpsnf1o  8914  card1  9928  pm54.43lem  9960  cf0  10211  sdom2en01  10262  cardeq0  10512  enqbreq2  10880  addcompr  10981  mulcompr  10983  axrrecex  11123  negeq0  11483  muleqadd  11829  crne0  12186  dfnn3  12207  xmulneg1  13236  hasheq0  14335  hashbc  14425  hashf1lem2  14428  hash2pwpr  14448  eqwrds3  14934  cjne0  15136  sqrt00  15236  sqrtmsq2i  15361  cbvsum  15668  cbvsumv  15669  fsump1i  15742  cbvprod  15886  cbvprodv  15887  bpoly2  16030  bpoly3  16031  bpoly4  16032  absefib  16173  efieq1re  16174  xpccatid  18156  sgrpidmnd  18673  smndex2dnrinv  18849  isnsg4  19106  opprdomnb  20633  selvval  22029  mat1dimelbas  22365  pmatcollpw3fi1lem1  22680  2ndcctbss  23349  ptcnp  23516  ovolgelb  25388  ioorinv  25484  dvcobr  25856  rolle  25901  dvfsumlem2  25940  plymul0or  26195  reeff1o  26364  sineq0  26440  coseq1  26441  1cubr  26759  atandm2  26794  atandm3  26795  efrlim  26886  efrlimOLD  26887  isppw  27031  ppiub  27122  lgsdinn0  27263  m1lgs  27306  elzs2  28294  elznns  28297  1p1e2s  28309  twocut  28316  uhgr2edg  29142  usgredg2vlem1  29159  usgredg2vlem2  29160  ushgredgedg  29163  ushgredgedgloop  29165  edgnbusgreu  29301  nb3grprlem2  29315  nb3gr2nb  29318  usgredgsscusgredg  29394  usgr2wlkneq  29693  usgr2pthlem  29700  crctcshwlkn0  29758  wwlksn0s  29798  umgr2adedgwlk  29882  umgr2adedgspth  29885  elwwlks2s3  29888  elwwlks2ons3im  29891  rusgrnumwwlkl1  29905  clwlkclwwlkflem  29940  isfrgr  30196  frgr3v  30211  frgrregorufr0  30260  isgrpo  30433  vciOLD  30497  chnlei  31421  h1de2ctlem  31491  cmcmlem  31527  cmcm2i  31529  cmbr2i  31532  osumcor2i  31580  pjss2i  31616  ho01i  31764  nmop0h  31927  pjclem1  32131  jplem1  32204  atabs2i  32338  1arithidom  33515  ply1dg1rt  33555  fedgmullem2  33633  ccfldextdgrr  33674  zarcls  33871  breprexp  34631  bnj168  34727  bnj927  34766  bnj543  34890  bnj970  34944  subfacp1lem6  35179  satfv1  35357  satfvsucsuc  35359  satf0  35366  fmlaomn0  35384  fmla0disjsuc  35392  satffunlem2lem1  35398  mppspstlem  35565  quad3  35664  brdomain  35928  brrange  35929  brimg  35932  brapply  35933  brsuccf  35936  brfullfun  35943  brrestrict  35944  rankeq1o  36166  sumeq2si  36197  prodeq2si  36199  cbvprodvw2  36242  bj-snsetex  36958  bj-reabeq  37022  bj-rest10  37083  bj-ismooredr2  37105  bj-pinftynminfty  37222  dffinxpf  37380  finxp0  37386  matunitlindflem1  37617  ismblfin  37662  opropabco  37725  fdc  37746  isdrngo1  37957  smprngopr  38053  qseq  38647  eldisjlem19  38809  cdleme25cv  40359  cdlemk35  40913  dicval2  41180  dicopelval2  41182  dicelval2N  41183  hdmap1fval  41797  sn-0tie0  42446  absnw  42673  mzpcompact2lem  42746  eldioph4b  42806  2nn0ind  42941  islmodfg  43065  abeqabi  43404  relintab  43579  brtrclfv2  43723  frege116  43975  elnev  44434  dvnprodlem1  45951  fourierdlem103  46214  fourierdlem104  46215  ovnovollem3  46663  fmtno4prmfac  47577  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2nb4  48030  usgrexmpl2nb5  48031  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  lindsrng01  48461  ldepspr  48466  nn0sumshdiglemB  48613  mofeu  48840  f1omo  48885