Theorem eqeq2i 2472

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

Syntax hints:   <-> wb 184   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

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

This theorem is referenced by:  eqeq12i  2474  eqtri  2483  neeq2i  2741  rabid2  3032  dfss2  3478  equncom  3635  rabrsn  4086  ssunpr  4178  sspr  4179  sstp  4180  preq12b  4192  preqsn  4199  opeqpr  4733  wefrc  4862  orddif  4960  dfrel4v  5442  dfiota2  5535  funopg  5602  funimaexg  5647  dffn5f  5903  fnressn  6059  fressnfv  6061  fnprb  6106  fnov  6383  ovmpt2s  6399  onuninsuci  6648  fvresex  6746  elxp6  6805  el2xptp  6816  el2xptp0  6817  opiota  6832  tpossym  6979  qsid  7369  mapsncnv  7458  ixpsnf1o  7502  card1  8340  pm54.43lem  8371  cf0  8622  sdom2en01  8673  cardeq0  8918  enqbreq2  9287  addcompr  9388  mulcompr  9390  axrrecex  9529  negeq0  9864  muleqadd  10189  crne0  10524  dfnn3  10545  xmulneg1  11464  hasheq0  12416  hashbc  12486  hashf1lem2  12489  hash2pwpr  12503  cjne0  13078  sqrt00  13179  sqrtmsq2i  13302  cbvsum  13599  fsump1i  13666  cbvprod  13804  absefib  14015  efieq1re  14016  xpccatid  15656  isnsg4  16443  mat1dimelbas  19140  pmatcollpw3fi1lem1  19454  2ndcctbss  20122  ptcnp  20289  ovolgelb  22057  ioorinv  22151  rolle  22557  plymul0or  22843  reeff1o  23008  sineq0  23080  coseq1  23081  1cubr  23370  atandm2  23405  atandm3  23406  efrlim  23497  isppw  23586  ppiub  23677  lgsdinn0  23813  m1lgs  23835  usgra2edg  24584  usgraedg4  24589  usgraidx2vlem1  24593  usgraidx2vlem2  24594  nb3graprlem2  24654  nb3grapr  24655  nb3grapr2  24656  nb3gra2nb  24657  2trllemH  24756  2trllemE  24757  usgrcyclnl2  24843  4cycl4dv  24869  wwlkn0  24891  wwlkn0s  24907  rusgranumwlkl1  25149  2pthfrgra  25213  isgrpo  25396  vci  25639  chnlei  26601  h1de2ctlem  26671  cmcmlem  26707  cmcm2i  26709  cmbr2i  26712  osumcor2i  26760  pjss2i  26796  ho01i  26945  nmop0h  27108  pjclem1  27312  jplem1  27385  atabs2i  27519  rabid2f  27599  preqsnd  27624  dfrel4  27668  subfacp1lem6  28893  mppspstlem  29195  quad3  29288  trpredmintr  29554  brdomain  29811  brrange  29812  brimg  29815  brapply  29816  brsuccf  29819  brfullfun  29826  brrestrict  29827  bpoly2  30047  bpoly3  30048  bpoly4  30049  rankeq1o  30056  ismblfin  30295  opropabco  30454  fdc  30478  isdrngo1  30599  smprngopr  30689  mzpcompact2lem  30923  eldioph4b  30984  2nn0ind  31120  islmodfg  31254  elnev  31586  dvnprodlem1  31982  fourierdlem103  32231  fourierdlem104  32232  usgra2pthlem1  32725  usgedgvadf1lem1  32785  usgedgvadf1lem2  32786  usgedgvadf1ALTlem1  32788  usgedgvadf1ALTlem2  32789  lindsrng01  33323  ldepspr  33328  nn0sumshdiglemB  33495  bnj168  34186  bnj927  34228  bnj543  34352  bnj970  34406  bj-snsetex  34922  bj-pinftynminfty  35030  cdleme25cv  36481  cdlemk35  37035  dicval2  37303  dicopelval2  37305  dicelval2N  37306  hdmap1fval  37921