Theorem eqeq2i 2750

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

Syntax hints:   ↔ wb 206   = wceq 1542

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeq12i  2755  eqtri  2760  neeq2i  2998  rabid2f  3432  rabid2im  3433  abv  3454  equncom  4113  eq0  4304  ab0w  4333  ab0  4334  ab0orv  4337  absn  4602  rabrsn  4683  ssunpr  4792  sspr  4793  sstp  4794  preq12b  4808  preqsnd  4817  preq12nebg  4821  opthprneg  4823  opeqpr  5461  propssopi  5464  wefrc  5626  dfrel4v  6156  dfrel4  6157  orddif  6423  funopg  6534  f1imadifssran  6586  funcocnv2  6807  dffn5f  6913  fnressn  7113  fressnfv  7115  fnprb  7164  fntpb  7165  riotaeqimp  7351  fnov  7499  ovmpos  7516  onuninsuci  7792  fvresex  7914  elxp6  7977  el2xptp  7989  el2xptp0  7990  opiota  8013  tpossym  8210  qsid  8730  mapsncnv  8843  ixpsnf1o  8888  card1  9892  pm54.43lem  9924  cf0  10173  sdom2en01  10224  cardeq0  10474  enqbreq2  10843  addcompr  10944  mulcompr  10946  axrrecex  11086  negeq0  11447  muleqadd  11793  crne0  12150  dfnn3  12171  xmulneg1  13196  hasheq0  14298  hashbc  14388  hashf1lem2  14391  hash2pwpr  14411  eqwrds3  14896  cjne0  15098  sqrt00  15198  sqrtmsq2i  15323  cbvsum  15630  cbvsumv  15631  fsump1i  15704  cbvprod  15848  cbvprodv  15849  bpoly2  15992  bpoly3  15993  bpoly4  15994  absefib  16135  efieq1re  16136  xpccatid  18123  sgrpidmnd  18676  smndex2dnrinv  18852  isnsg4  19108  opprdomnb  20662  selvval  22090  mat1dimelbas  22427  pmatcollpw3fi1lem1  22742  2ndcctbss  23411  ptcnp  23578  ovolgelb  25449  ioorinv  25545  dvcobr  25917  rolle  25962  dvfsumlem2  26001  plymul0or  26256  reeff1o  26425  sineq0  26501  coseq1  26502  1cubr  26820  atandm2  26855  atandm3  26856  efrlim  26947  efrlimOLD  26948  isppw  27092  ppiub  27183  lgsdinn0  27324  m1lgs  27367  elzs2  28407  elznns  28410  twocut  28431  uhgr2edg  29293  usgredg2vlem1  29310  usgredg2vlem2  29311  ushgredgedg  29314  ushgredgedgloop  29316  edgnbusgreu  29452  nb3grprlem2  29466  nb3gr2nb  29469  usgredgsscusgredg  29545  usgr2wlkneq  29841  usgr2pthlem  29848  crctcshwlkn0  29906  wwlksn0s  29946  umgr2adedgwlk  30030  umgr2adedgspth  30033  elwwlks2s3  30036  elwwlks2ons3im  30039  rusgrnumwwlkl1  30056  clwlkclwwlkflem  30091  isfrgr  30347  frgr3v  30362  frgrregorufr0  30411  isgrpo  30585  vciOLD  30649  chnlei  31573  h1de2ctlem  31643  cmcmlem  31679  cmcm2i  31681  cmbr2i  31684  osumcor2i  31732  pjss2i  31768  ho01i  31916  nmop0h  32079  pjclem1  32283  jplem1  32356  atabs2i  32490  1arithidom  33630  ply1dg1rt  33673  esplyfval1  33750  vieta  33757  fedgmullem2  33808  ccfldextdgrr  33850  zarcls  34052  breprexp  34811  bnj168  34907  bnj927  34946  bnj543  35069  bnj970  35123  subfacp1lem6  35401  satfv1  35579  satfvsucsuc  35581  satf0  35588  fmlaomn0  35606  fmla0disjsuc  35614  satffunlem2lem1  35620  mppspstlem  35787  quad3  35886  brdomain  36147  brrange  36148  brimg  36151  brapply  36152  lemsuccf  36155  brfullfun  36164  brrestrict  36165  rankeq1o  36387  sumeq2si  36418  prodeq2si  36420  cbvprodvw2  36463  bj-snsetex  37211  bj-reabeq  37275  bj-rest10  37341  bj-ismooredr2  37363  bj-pinftynminfty  37482  dffinxpf  37640  finxp0  37646  matunitlindflem1  37867  ismblfin  37912  opropabco  37975  fdc  37996  isdrngo1  38207  smprngopr  38303  qseq  38984  eldisjlem19  39164  cdleme25cv  40734  cdlemk35  41288  dicval2  41555  dicopelval2  41557  dicelval2N  41558  hdmap1fval  42172  sn-0tie0  42821  absnw  43036  mzpcompact2lem  43108  eldioph4b  43168  2nn0ind  43302  islmodfg  43426  abeqabi  43764  relintab  43939  brtrclfv2  44083  frege116  44335  elnev  44793  dvnprodlem1  46304  fourierdlem103  46567  fourierdlem104  46568  ovnovollem3  47016  fmtno4prmfac  47932  usgrexmpl2nb1  48392  usgrexmpl2nb2  48393  usgrexmpl2nb3  48394  usgrexmpl2nb4  48395  usgrexmpl2nb5  48396  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5lem3  48482  lindsrng01  48828  ldepspr  48833  nn0sumshdiglemB  48980  mofeu  49207  f1omo  49252