Theorem eqeq2i 2749

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 2748	. 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 2123  ax-ext 2708

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

This theorem is referenced by:  eqeq12i  2754  eqtri  2759  neeq2i  2997  rabid2f  3430  rabid2im  3431  abv  3452  equncom  4111  eq0  4302  ab0w  4331  ab0  4332  ab0orv  4335  absn  4600  rabrsn  4681  ssunpr  4790  sspr  4791  sstp  4792  preq12b  4806  preqsnd  4815  preq12nebg  4819  opthprneg  4821  opeqpr  5453  propssopi  5456  wefrc  5618  dfrel4v  6148  dfrel4  6149  orddif  6415  funopg  6526  f1imadifssran  6578  funcocnv2  6799  dffn5f  6905  fnressn  7103  fressnfv  7105  fnprb  7154  fntpb  7155  riotaeqimp  7341  fnov  7489  ovmpos  7506  onuninsuci  7782  fvresex  7904  elxp6  7967  el2xptp  7979  el2xptp0  7980  opiota  8003  tpossym  8200  qsid  8718  mapsncnv  8831  ixpsnf1o  8876  card1  9880  pm54.43lem  9912  cf0  10161  sdom2en01  10212  cardeq0  10462  enqbreq2  10831  addcompr  10932  mulcompr  10934  axrrecex  11074  negeq0  11435  muleqadd  11781  crne0  12138  dfnn3  12159  xmulneg1  13184  hasheq0  14286  hashbc  14376  hashf1lem2  14379  hash2pwpr  14399  eqwrds3  14884  cjne0  15086  sqrt00  15186  sqrtmsq2i  15311  cbvsum  15618  cbvsumv  15619  fsump1i  15692  cbvprod  15836  cbvprodv  15837  bpoly2  15980  bpoly3  15981  bpoly4  15982  absefib  16123  efieq1re  16124  xpccatid  18111  sgrpidmnd  18664  smndex2dnrinv  18840  isnsg4  19096  opprdomnb  20650  selvval  22078  mat1dimelbas  22415  pmatcollpw3fi1lem1  22730  2ndcctbss  23399  ptcnp  23566  ovolgelb  25437  ioorinv  25533  dvcobr  25905  rolle  25950  dvfsumlem2  25989  plymul0or  26244  reeff1o  26413  sineq0  26489  coseq1  26490  1cubr  26808  atandm2  26843  atandm3  26844  efrlim  26935  efrlimOLD  26936  isppw  27080  ppiub  27171  lgsdinn0  27312  m1lgs  27355  elzs2  28395  elznns  28398  twocut  28419  uhgr2edg  29281  usgredg2vlem1  29298  usgredg2vlem2  29299  ushgredgedg  29302  ushgredgedgloop  29304  edgnbusgreu  29440  nb3grprlem2  29454  nb3gr2nb  29457  usgredgsscusgredg  29533  usgr2wlkneq  29829  usgr2pthlem  29836  crctcshwlkn0  29894  wwlksn0s  29934  umgr2adedgwlk  30018  umgr2adedgspth  30021  elwwlks2s3  30024  elwwlks2ons3im  30027  rusgrnumwwlkl1  30044  clwlkclwwlkflem  30079  isfrgr  30335  frgr3v  30350  frgrregorufr0  30399  isgrpo  30572  vciOLD  30636  chnlei  31560  h1de2ctlem  31630  cmcmlem  31666  cmcm2i  31668  cmbr2i  31671  osumcor2i  31719  pjss2i  31755  ho01i  31903  nmop0h  32066  pjclem1  32270  jplem1  32343  atabs2i  32477  1arithidom  33618  ply1dg1rt  33661  vieta  33736  fedgmullem2  33787  ccfldextdgrr  33829  zarcls  34031  breprexp  34790  bnj168  34886  bnj927  34925  bnj543  35049  bnj970  35103  subfacp1lem6  35379  satfv1  35557  satfvsucsuc  35559  satf0  35566  fmlaomn0  35584  fmla0disjsuc  35592  satffunlem2lem1  35598  mppspstlem  35765  quad3  35864  brdomain  36125  brrange  36126  brimg  36129  brapply  36130  lemsuccf  36133  brfullfun  36142  brrestrict  36143  rankeq1o  36365  sumeq2si  36396  prodeq2si  36398  cbvprodvw2  36441  bj-snsetex  37164  bj-reabeq  37228  bj-rest10  37293  bj-ismooredr2  37315  bj-pinftynminfty  37432  dffinxpf  37590  finxp0  37596  matunitlindflem1  37817  ismblfin  37862  opropabco  37925  fdc  37946  isdrngo1  38157  smprngopr  38253  qseq  38907  eldisjlem19  39069  cdleme25cv  40618  cdlemk35  41172  dicval2  41439  dicopelval2  41441  dicelval2N  41442  hdmap1fval  42056  sn-0tie0  42706  absnw  42921  mzpcompact2lem  42993  eldioph4b  43053  2nn0ind  43187  islmodfg  43311  abeqabi  43649  relintab  43824  brtrclfv2  43968  frege116  44220  elnev  44678  dvnprodlem1  46190  fourierdlem103  46453  fourierdlem104  46454  ovnovollem3  46902  fmtno4prmfac  47818  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  usgrexmpl2nb3  48280  usgrexmpl2nb4  48281  usgrexmpl2nb5  48282  pgnioedg1  48354  pgnioedg2  48355  pgnioedg3  48356  pgnioedg4  48357  pgnioedg5  48358  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  lindsrng01  48714  ldepspr  48719  nn0sumshdiglemB  48866  mofeu  49093  f1omo  49138