Theorem eqeq2i 2776

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

Syntax hints:   ↔ wb 209   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqeq12i  2781  eqtri  2786  neeq2i  3023  rabid2f  3447  rabid2im  3448  abv  3467  equncom  4113  eq0  4304  ab0w  4335  ab0  4336  ab0orv  4339  absn  4609  rabrsn  4690  ssunpr  4799  sspr  4800  sstp  4801  preq12b  4815  preqsnd  4824  preq12nebg  4828  opthprneg  4830  opeqpr  5488  propssopi  5491  wefrc  5655  dfrel4v  6188  dfrel4  6189  orddif  6459  funopg  6570  funcocnv2  6846  dffn5f  6952  fnressn  7155  fressnfv  7157  fnprb  7206  fntpb  7207  riotaeqimp  7393  fnov  7541  ovmpos  7558  onuninsuci  7832  fvresex  7953  elxp6  8016  el2xptp  8028  el2xptp0  8029  opiota  8052  tpossym  8250  qsid  8775  mapsncnv  8887  ixpsnf1o  8932  card1  9950  pm54.43lem  9982  cf0  10229  sdom2en01  10281  cardeq0  10531  enqbreq2  10900  addcompr  11001  mulcompr  11003  axrrecex  11143  negeq0  11507  muleqadd  11853  crne0  12206  dfnn3  12242  xmulneg1  13290  hasheq0  14395  hashbc  14486  hashf1lem2  14489  hash2pwpr  14509  eqwrds3  14994  cjne0  15210  sqrt00  15310  sqrtmsq2i  15435  cbvsum  15742  cbvsumv  15743  fsump1i  15816  cbvprod  15963  cbvprodv  15964  bpoly2  16106  bpoly3  16107  bpoly4  16108  absefib  16249  efieq1re  16250  xpccatid  18239  sgrpidmnd  18792  smndex2dnrinv  18972  isnsg4  19228  opprdomnb  20815  selvval  22271  mat1dimelbas  22628  pmatcollpw3fi1lem1  22943  2ndcctbss  23612  ptcnp  23779  ovolgelb  25639  ioorinv  25735  dvcobr  26105  rolle  26149  dvfsumlem2  26186  plymul0or  26439  reeff1o  26610  sineq0  26689  coseq1  26690  1cubr  27007  atandm2  27042  atandm3  27043  efrlim  27134  isppw  27278  ppiub  27368  lgsdinn0  27509  m1lgs  27552  elzs2  28592  elznns  28595  twocut  28616  uhgr2edg  29558  usgredg2vlem1  29575  usgredg2vlem2  29576  ushgredgedg  29579  ushgredgedgloop  29581  edgnbusgreu  29717  nb3grprlem2  29731  nb3gr2nb  29734  usgredgsscusgredg  29809  usgr2wlkneq  30105  usgr2pthlem  30112  crctcshwlkn0  30170  wwlksn0s  30210  umgr2adedgwlk  30294  umgr2adedgspth  30297  elwwlks2s3  30300  elwwlks2ons3im  30303  rusgrnumwwlkl1  30320  clwlkclwwlkflem  30355  isfrgr  30611  frgr3v  30626  frgrregorufr0  30675  isgrpo  30849  vciOLD  30913  chnlei  31837  h1de2ctlem  31907  cmcmlem  31943  cmcm2i  31945  cmbr2i  31948  osumcor2i  31996  pjss2i  32032  ho01i  32180  nmop0h  32343  pjclem1  32547  jplem1  32620  atabs2i  32754  1arithidom  33827  ply1dg1rt  33870  selvply1rhmlem2  33911  esplyfval1  33963  vieta  33970  fedgmullem2  34020  ccfldextdgrr  34062  zarcls  34264  breprexp  35020  bnj168  35119  bnj927  35158  bnj543  35281  bnj970  35335  subfacp1lem6  35677  satfv1  35855  satfvsucsuc  35857  satf0  35864  fmlaomn0  35882  fmla0disjsuc  35890  satffunlem2lem1  35896  mppspstlem  36063  quad3  36162  brdomain  36423  brrange  36424  brimg  36427  brapply  36428  lemsuccf  36431  brfullfun  36440  brrestrict  36441  rankeq1o  36663  sumeq2si  36734  prodeq2si  36736  cbvprodvw2  36779  bj-snsetex  37619  bj-reabeq  37683  bj-rest10  37750  bj-ismooredr2  37772  bj-pinftynminfty  37891  dffinxpf  38051  finxp0  38057  matunitlindflem1  38287  ismblfin  38332  opropabco  38395  fdc  38416  isdrngo1  38627  smprngopr  38723  qseq  39402  eldisjlem19  39582  cdleme25cv  41152  cdlemk35  41706  dicval2  41973  dicopelval2  41975  dicelval2N  41976  hdmap1fval  42590  sn-0tie0  43245  absnw  43430  mzpcompact2lem  43502  eldioph4b  43558  2nn0ind  43692  islmodfg  43816  abeqabi  44154  relintab  44329  brtrclfv2  44473  frege116  44725  elnev  45167  dvnprodlem1  46680  fourierdlem103  46943  fourierdlem104  46944  ovnovollem3  47392  fmtno4prmfac  48344  usgrexmpl2nb1  48817  usgrexmpl2nb2  48818  usgrexmpl2nb3  48819  usgrexmpl2nb4  48820  usgrexmpl2nb5  48821  pgnioedg1  48893  pgnioedg2  48894  pgnioedg3  48895  pgnioedg4  48896  pgnioedg5  48897  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  pgnbgreunbgrlem2lem3  48901  pgnbgreunbgrlem5lem1  48905  pgnbgreunbgrlem5lem2  48906  pgnbgreunbgrlem5lem3  48907  smprngprmrng  49124  lindsrng01  49268  ldepspr  49273  nn0sumshdiglemB  49420  mofeu  49646  f1omo  49691