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 206   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  eqeq12i  2749  eqtri  2754  neeq2i  2993  rabid2f  3426  rabid2im  3427  abv  3448  equncom  4106  eq0  4297  ab0w  4326  ab0  4327  ab0orv  4330  eq0rdv  4354  rzal  4456  absn  4593  rabrsn  4674  ssunpr  4783  sspr  4784  sstp  4785  preq12b  4799  preqsnd  4808  preq12nebg  4812  opthprneg  4814  opeqpr  5443  propssopi  5446  wefrc  5608  dfrel4v  6137  dfrel4  6138  orddif  6404  funopg  6515  f1imadifssran  6567  funcocnv2  6788  dffn5f  6893  fnressn  7091  fressnfv  7093  fnprb  7142  fntpb  7143  riotaeqimp  7329  fnov  7477  ovmpos  7494  onuninsuci  7770  fvresex  7892  elxp6  7955  el2xptp  7967  el2xptp0  7968  opiota  7991  tpossym  8188  qsid  8705  mapsncnv  8817  ixpsnf1o  8862  card1  9861  pm54.43lem  9893  cf0  10142  sdom2en01  10193  cardeq0  10443  enqbreq2  10811  addcompr  10912  mulcompr  10914  axrrecex  11054  negeq0  11415  muleqadd  11761  crne0  12118  dfnn3  12139  xmulneg1  13168  hasheq0  14270  hashbc  14360  hashf1lem2  14363  hash2pwpr  14383  eqwrds3  14868  cjne0  15070  sqrt00  15170  sqrtmsq2i  15295  cbvsum  15602  cbvsumv  15603  fsump1i  15676  cbvprod  15820  cbvprodv  15821  bpoly2  15964  bpoly3  15965  bpoly4  15966  absefib  16107  efieq1re  16108  xpccatid  18094  sgrpidmnd  18647  smndex2dnrinv  18823  isnsg4  19079  opprdomnb  20632  selvval  22050  mat1dimelbas  22386  pmatcollpw3fi1lem1  22701  2ndcctbss  23370  ptcnp  23537  ovolgelb  25408  ioorinv  25504  dvcobr  25876  rolle  25921  dvfsumlem2  25960  plymul0or  26215  reeff1o  26384  sineq0  26460  coseq1  26461  1cubr  26779  atandm2  26814  atandm3  26815  efrlim  26906  efrlimOLD  26907  isppw  27051  ppiub  27142  lgsdinn0  27283  m1lgs  27326  elzs2  28323  elznns  28326  1p1e2s  28339  twocut  28346  uhgr2edg  29186  usgredg2vlem1  29203  usgredg2vlem2  29204  ushgredgedg  29207  ushgredgedgloop  29209  edgnbusgreu  29345  nb3grprlem2  29359  nb3gr2nb  29362  usgredgsscusgredg  29438  usgr2wlkneq  29734  usgr2pthlem  29741  crctcshwlkn0  29799  wwlksn0s  29839  umgr2adedgwlk  29923  umgr2adedgspth  29926  elwwlks2s3  29929  elwwlks2ons3im  29932  rusgrnumwwlkl1  29949  clwlkclwwlkflem  29984  isfrgr  30240  frgr3v  30255  frgrregorufr0  30304  isgrpo  30477  vciOLD  30541  chnlei  31465  h1de2ctlem  31535  cmcmlem  31571  cmcm2i  31573  cmbr2i  31576  osumcor2i  31624  pjss2i  31660  ho01i  31808  nmop0h  31971  pjclem1  32175  jplem1  32248  atabs2i  32382  1arithidom  33502  ply1dg1rt  33543  fedgmullem2  33643  ccfldextdgrr  33685  zarcls  33887  breprexp  34646  bnj168  34742  bnj927  34781  bnj543  34905  bnj970  34959  subfacp1lem6  35229  satfv1  35407  satfvsucsuc  35409  satf0  35416  fmlaomn0  35434  fmla0disjsuc  35442  satffunlem2lem1  35448  mppspstlem  35615  quad3  35714  brdomain  35975  brrange  35976  brimg  35979  brapply  35980  brsuccf  35983  brfullfun  35990  brrestrict  35991  rankeq1o  36213  sumeq2si  36244  prodeq2si  36246  cbvprodvw2  36289  bj-snsetex  37005  bj-reabeq  37069  bj-rest10  37130  bj-ismooredr2  37152  bj-pinftynminfty  37269  dffinxpf  37427  finxp0  37433  matunitlindflem1  37664  ismblfin  37709  opropabco  37772  fdc  37793  isdrngo1  38004  smprngopr  38100  qseq  38694  eldisjlem19  38856  cdleme25cv  40405  cdlemk35  40959  dicval2  41226  dicopelval2  41228  dicelval2N  41229  hdmap1fval  41843  sn-0tie0  42492  absnw  42719  mzpcompact2lem  42792  eldioph4b  42852  2nn0ind  42986  islmodfg  43110  abeqabi  43449  relintab  43624  brtrclfv2  43768  frege116  44020  elnev  44478  dvnprodlem1  45992  fourierdlem103  46255  fourierdlem104  46256  ovnovollem3  46704  fmtno4prmfac  47611  usgrexmpl2nb1  48071  usgrexmpl2nb2  48072  usgrexmpl2nb3  48073  usgrexmpl2nb4  48074  usgrexmpl2nb5  48075  pgnioedg1  48147  pgnioedg2  48148  pgnioedg3  48149  pgnioedg4  48150  pgnioedg5  48151  pgnbgreunbgrlem2lem1  48153  pgnbgreunbgrlem2lem2  48154  pgnbgreunbgrlem2lem3  48155  pgnbgreunbgrlem5lem1  48159  pgnbgreunbgrlem5lem2  48160  pgnbgreunbgrlem5lem3  48161  lindsrng01  48508  ldepspr  48513  nn0sumshdiglemB  48660  mofeu  48887  f1omo  48932