Theorem eqeq2i 2459

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 2456	. 2 |- ( A = B -> ( C = A <-> C = B ) )
3	1, 2	ax-mp 5	1 |- ( C = A <-> C = B )

Syntax hints:   <-> wb 184   = wceq 1381

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-cleq 2433

This theorem is referenced by:  eqeq12i  2461  eqtri  2470  neeq2i  2728  rabid2  3019  dfss2  3475  equncom  3631  rabrsn  4081  ssunpr  4173  sspr  4174  sstp  4175  preq12b  4187  preqsn  4194  opeqpr  4730  wefrc  4859  orddif  4957  dfrel4v  5444  dfiota2  5538  funopg  5606  funimaexg  5651  dffn5f  5909  fnressn  6064  fressnfv  6066  fnprb  6110  fnov  6391  ovmpt2s  6407  onuninsuci  6656  fvresex  6754  elxp6  6813  el2xptp  6824  el2xptp0  6825  opiota  6840  tpossym  6985  qsid  7375  mapsncnv  7463  ixpsnf1o  7507  card1  8347  pm54.43lem  8378  cf0  8629  sdom2en01  8680  cardeq0  8925  enqbreq2  9296  addcompr  9397  mulcompr  9399  axrrecex  9538  negeq0  9873  muleqadd  10194  crne0  10530  dfnn3  10551  xmulneg1  11465  hasheq0  12407  hashbc  12476  hashf1lem2  12479  hash2pwpr  12493  cjne0  12970  sqrt00  13071  sqrtmsq2i  13194  cbvsum  13491  fsump1i  13558  absefib  13805  efieq1re  13806  xpccatid  15326  isnsg4  16113  mat1dimelbas  18840  pmatcollpw3fi1lem1  19154  2ndcctbss  19822  ptcnp  19989  ovolgelb  21757  ioorinv  21851  rolle  22257  plymul0or  22542  reeff1o  22707  sineq0  22779  coseq1  22780  1cubr  23038  atandm2  23073  atandm3  23074  efrlim  23164  isppw  23253  ppiub  23344  lgsdinn0  23480  m1lgs  23502  usgra2edg  24247  usgraedg4  24252  usgraidx2vlem1  24256  usgraidx2vlem2  24257  nb3graprlem2  24317  nb3grapr  24318  nb3grapr2  24319  nb3gra2nb  24320  2trllemH  24419  2trllemE  24420  usgrcyclnl2  24506  4cycl4dv  24532  wwlkn0  24554  wwlkn0s  24570  rusgranumwlkl1  24812  2pthfrgra  24876  isgrpo  25063  vci  25306  chnlei  26268  h1de2ctlem  26338  cmcmlem  26374  cmcm2i  26376  cmbr2i  26379  osumcor2i  26427  pjss2i  26463  ho01i  26612  nmop0h  26775  pjclem1  26979  jplem1  27052  atabs2i  27186  rabid2f  27265  preqsnd  27283  dfrel4  27319  subfacp1lem6  28495  mppspstlem  28797  quad3  28890  cbvprod  29015  trpredmintr  29282  brdomain  29551  brrange  29552  brimg  29555  brapply  29556  brsuccf  29559  brfullfun  29566  brrestrict  29567  bpoly2  29787  bpoly3  29788  bpoly4  29789  rankeq1o  29796  ismblfin  30023  opropabco  30182  fdc  30206  isdrngo1  30327  smprngopr  30417  mzpcompact2lem  30652  eldioph4b  30713  2nn0ind  30849  islmodfg  30983  elnev  31292  fourierdlem103  31877  fourierdlem104  31878  usgra2pthlem1  32187  usgedgvadf1lem1  32247  usgedgvadf1lem2  32248  usgedgvadf1ALTlem1  32250  usgedgvadf1ALTlem2  32251  lindsrng01  32779  ldepspr  32784  bnj168  33493  bnj927  33534  bnj543  33658  bnj970  33712  bj-snsetex  34233  bj-pinftynminfty  34332  cdleme25cv  35786  cdlemk35  36340  dicval2  36608  dicopelval2  36610  dicelval2N  36611  hdmap1fval  37226