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  3421  rabid2im  3422  abv  3442  equncom  4100  eq0  4291  ab0w  4320  ab0  4321  ab0orv  4324  absn  4588  rabrsn  4669  ssunpr  4778  sspr  4779  sstp  4780  preq12b  4794  preqsnd  4803  preq12nebg  4807  opthprneg  4809  opeqpr  5454  propssopi  5457  wefrc  5619  dfrel4v  6149  dfrel4  6150  orddif  6416  funopg  6527  f1imadifssran  6579  funcocnv2  6800  dffn5f  6906  fnressn  7106  fressnfv  7108  fnprb  7157  fntpb  7158  riotaeqimp  7344  fnov  7492  ovmpos  7509  onuninsuci  7785  fvresex  7907  elxp6  7970  el2xptp  7982  el2xptp0  7983  opiota  8006  tpossym  8202  qsid  8722  mapsncnv  8835  ixpsnf1o  8880  card1  9886  pm54.43lem  9918  cf0  10167  sdom2en01  10218  cardeq0  10468  enqbreq2  10837  addcompr  10938  mulcompr  10940  axrrecex  11080  negeq0  11442  muleqadd  11788  crne0  12146  dfnn3  12182  xmulneg1  13215  hasheq0  14319  hashbc  14409  hashf1lem2  14412  hash2pwpr  14432  eqwrds3  14917  cjne0  15119  sqrt00  15219  sqrtmsq2i  15344  cbvsum  15651  cbvsumv  15652  fsump1i  15725  cbvprod  15872  cbvprodv  15873  bpoly2  16016  bpoly3  16017  bpoly4  16018  absefib  16159  efieq1re  16160  xpccatid  18148  sgrpidmnd  18701  smndex2dnrinv  18880  isnsg4  19136  opprdomnb  20688  selvval  22114  mat1dimelbas  22449  pmatcollpw3fi1lem1  22764  2ndcctbss  23433  ptcnp  23600  ovolgelb  25460  ioorinv  25556  dvcobr  25926  rolle  25970  dvfsumlem2  26007  plymul0or  26260  reeff1o  26428  sineq0  26504  coseq1  26505  1cubr  26822  atandm2  26857  atandm3  26858  efrlim  26949  efrlimOLD  26950  isppw  27094  ppiub  27184  lgsdinn0  27325  m1lgs  27368  elzs2  28408  elznns  28411  twocut  28432  uhgr2edg  29294  usgredg2vlem1  29311  usgredg2vlem2  29312  ushgredgedg  29315  ushgredgedgloop  29317  edgnbusgreu  29453  nb3grprlem2  29467  nb3gr2nb  29470  usgredgsscusgredg  29546  usgr2wlkneq  29842  usgr2pthlem  29849  crctcshwlkn0  29907  wwlksn0s  29947  umgr2adedgwlk  30031  umgr2adedgspth  30034  elwwlks2s3  30037  elwwlks2ons3im  30040  rusgrnumwwlkl1  30057  clwlkclwwlkflem  30092  isfrgr  30348  frgr3v  30363  frgrregorufr0  30412  isgrpo  30586  vciOLD  30650  chnlei  31574  h1de2ctlem  31644  cmcmlem  31680  cmcm2i  31682  cmbr2i  31685  osumcor2i  31733  pjss2i  31769  ho01i  31917  nmop0h  32080  pjclem1  32284  jplem1  32357  atabs2i  32491  1arithidom  33615  ply1dg1rt  33658  esplyfval1  33735  vieta  33742  fedgmullem2  33793  ccfldextdgrr  33835  zarcls  34037  breprexp  34796  bnj168  34892  bnj927  34931  bnj543  35054  bnj970  35108  subfacp1lem6  35386  satfv1  35564  satfvsucsuc  35566  satf0  35573  fmlaomn0  35591  fmla0disjsuc  35599  satffunlem2lem1  35605  mppspstlem  35772  quad3  35871  brdomain  36132  brrange  36133  brimg  36136  brapply  36137  lemsuccf  36140  brfullfun  36149  brrestrict  36150  rankeq1o  36372  sumeq2si  36403  prodeq2si  36405  cbvprodvw2  36448  bj-snsetex  37289  bj-reabeq  37353  bj-rest10  37419  bj-ismooredr2  37441  bj-pinftynminfty  37560  dffinxpf  37718  finxp0  37724  matunitlindflem1  37954  ismblfin  37999  opropabco  38062  fdc  38083  isdrngo1  38294  smprngopr  38390  qseq  39071  eldisjlem19  39251  cdleme25cv  40821  cdlemk35  41375  dicval2  41642  dicopelval2  41644  dicelval2N  41645  hdmap1fval  42259  sn-0tie0  42913  absnw  43128  mzpcompact2lem  43200  eldioph4b  43260  2nn0ind  43394  islmodfg  43518  abeqabi  43856  relintab  44031  brtrclfv2  44175  frege116  44427  elnev  44885  dvnprodlem1  46395  fourierdlem103  46658  fourierdlem104  46659  ovnovollem3  47107  fmtno4prmfac  48050  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2nb3  48525  usgrexmpl2nb4  48526  usgrexmpl2nb5  48527  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  lindsrng01  48959  ldepspr  48964  nn0sumshdiglemB  49111  mofeu  49338  f1omo  49383