Theorem eqeq2i 2463

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)

Hypothesis

Ref	Expression
eqeq2i.1	|- A = B

Assertion

Ref	Expression
eqeq2i	|- ( C = A <-> C = B )

Proof of Theorem eqeq2i

Step	Hyp	Ref	Expression
1		eqeq2i.1	. 2 |- A = B
2		eqeq2 2462	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	ax-mp 5	1 |- ( C = A <-> C = B )

Syntax hints:   <-> wb 188   = wceq 1444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444

This theorem is referenced by:  eqeq12i  2465  eqtri  2473  neeq2i  2689  rabid2  2968  dfss2  3421  equncom  3579  rabrsn  4042  ssunpr  4134  sspr  4135  sstp  4136  preq12b  4151  preqsnd  4158  preqsn  4159  opeqpr  4698  wefrc  4828  dfrel4v  5287  orddif  5516  dfiota2  5547  funopg  5614  funimaexg  5660  dffn5f  5920  fnressn  6076  fressnfv  6078  fnprb  6123  fnov  6404  ovmpt2s  6420  onuninsuci  6667  fvresex  6766  elxp6  6825  el2xptp  6836  el2xptp0  6837  opiota  6852  tpossym  7005  qsid  7429  mapsncnv  7518  ixpsnf1o  7562  card1  8402  pm54.43lem  8433  cf0  8681  sdom2en01  8732  cardeq0  8977  enqbreq2  9345  addcompr  9446  mulcompr  9448  axrrecex  9587  negeq0  9928  muleqadd  10256  crne0  10602  dfnn3  10623  xmulneg1  11555  hasheq0  12544  hashbc  12616  hashf1lem2  12619  hash2pwpr  12635  cjne0  13226  sqrt00  13327  sqrtmsq2i  13450  cbvsum  13761  fsump1i  13830  cbvprod  13969  bpoly2  14110  bpoly3  14111  bpoly4  14112  absefib  14252  efieq1re  14253  xpccatid  16073  isnsg4  16860  mat1dimelbas  19496  pmatcollpw3fi1lem1  19810  2ndcctbss  20470  ptcnp  20637  ovolgelb  22433  ioorinv  22528  ioorinvOLD  22533  rolle  22942  plymul0or  23234  reeff1o  23402  sineq0  23476  coseq1  23477  1cubr  23768  atandm2  23803  atandm3  23804  efrlim  23895  isppw  24041  ppiub  24132  lgsdinn0  24268  m1lgs  24290  usgra2edg  25109  usgraedg4  25114  usgraidx2vlem1  25118  usgraidx2vlem2  25119  nb3graprlem2  25180  nb3grapr  25181  nb3grapr2  25182  nb3gra2nb  25183  2trllemH  25282  2trllemE  25283  usgrcyclnl2  25369  4cycl4dv  25395  wwlkn0  25417  wwlkn0s  25433  rusgranumwlkl1  25675  2pthfrgra  25739  isgrpo  25924  vci  26167  chnlei  27138  h1de2ctlem  27208  cmcmlem  27244  cmcm2i  27246  cmbr2i  27249  osumcor2i  27297  pjss2i  27333  ho01i  27481  nmop0h  27644  pjclem1  27848  jplem1  27921  atabs2i  28055  rabid2f  28136  dfrel4  28208  bnj168  29538  bnj927  29580  bnj543  29704  bnj970  29758  subfacp1lem6  29908  mppspstlem  30209  quad3  30302  trpredmintr  30472  brdomain  30700  brrange  30701  brimg  30704  brapply  30705  brsuccf  30708  brfullfun  30715  brrestrict  30716  rankeq1o  30938  bj-snsetex  31557  bj-pinftynminfty  31669  dffinxpf  31777  finxp0  31783  ismblfin  31981  opropabco  32050  fdc  32074  isdrngo1  32195  smprngopr  32285  cdleme25cv  33925  cdlemk35  34479  dicval2  34747  dicopelval2  34749  dicelval2N  34750  hdmap1fval  35365  mzpcompact2lem  35593  eldioph4b  35654  2nn0ind  35793  islmodfg  35927  relintab  36189  brtrclfv2  36319  frege116  36575  elnev  36789  dvnprodlem1  37821  fourierdlem103  38073  fourierdlem104  38074  propssopi  39000  riotaeqimp  39037  usgr2edg  39291  usgredg2vlem1  39302  usgredg2vlem2  39303  ushgredgedga  39306  ushgredgedgaloop  39308  edgnbusgreu  39441  nb3grprlem2  39455  nb3gr2nb  39458  usgredgsscusgredg  39520  usgra2pthlem1  39720  usgedgvadf1lem1  39778  usgedgvadf1lem2  39779  usgedgvadf1ALTlem1  39781  usgedgvadf1ALTlem2  39782  lindsrng01  40314  ldepspr  40319  nn0sumshdiglemB  40484