Theorem eqeq2i 2451

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

Syntax hints:   <-> wb 184   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2434

This theorem is referenced by:  eqtri  2461  rabid2  2896  dfss2  3343  equncom  3499  rabrsn  3943  ssunpr  4033  sspr  4034  sstp  4035  preq12b  4046  preqsn  4053  opeqpr  4586  wefrc  4712  orddif  4810  dfrel4v  5287  dfiota2  5380  funopg  5448  funimaexg  5493  dffn5f  5744  fnressn  5892  fressnfv  5894  fnprb  5934  fnov  6196  ovmpt2s  6212  onuninsuci  6449  fvresex  6548  elxp6  6606  opiota  6631  tpossym  6775  qsid  7164  mapsncnv  7257  ixpsnf1o  7301  card1  8136  pm54.43lem  8167  cf0  8418  sdom2en01  8469  cardeq0  8714  enqbreq2  9087  addcompr  9188  mulcompr  9190  axrrecex  9328  negeq0  9661  muleqadd  9978  crne0  10313  dfnn3  10334  xmulneg1  11230  hasheq0  12129  euhash1  12170  hash2pwpr  12180  hashbc  12204  hashf1lem2  12207  cjne0  12650  sqr00  12751  sqrmsq2i  12873  cbvsum  13170  fsump1i  13234  absefib  13480  efieq1re  13481  xpccatid  14996  isnsg4  15722  2ndcctbss  19057  ptcnp  19193  ovolgelb  20961  ioorinv  21054  rolle  21460  plymul0or  21745  reeff1o  21910  sineq0  21981  coseq1  21982  1cubr  22235  atandm2  22270  atandm3  22271  efrlim  22361  isppw  22450  ppiub  22541  lgsdinn0  22677  m1lgs  22699  usgra2edg  23299  usgraedg4  23303  usgraidx2vlem1  23307  usgraidx2vlem2  23308  nb3graprlem2  23358  nb3grapr  23359  nb3grapr2  23360  nb3gra2nb  23361  2trllemH  23449  2trllemE  23450  usgrcyclnl2  23525  4cycl4dv  23551  isgrpo  23681  vci  23924  chnlei  24886  h1de2ctlem  24956  cmcmlem  24992  cmcm2i  24994  cmbr2i  24997  osumcor2i  25045  pjss2i  25081  ho01i  25230  nmop0h  25393  pjclem1  25597  jplem1  25670  atabs2i  25804  rabid2f  25883  preqsnd  25899  dfrel4  25935  subfacp1lem6  27071  quad3  27301  cbvprod  27426  trpredmintr  27693  brdomain  27962  brrange  27963  brimg  27966  brapply  27967  brsuccf  27970  brfullfun  27977  brrestrict  27978  bpoly2  28198  bpoly3  28199  bpoly4  28200  rankeq1o  28207  ismblfin  28429  opropabco  28614  fdc  28638  isdrngo1  28759  smprngopr  28849  mzpcompact2lem  29085  eldioph4b  29147  2nn0ind  29283  islmodfg  29419  elnev  29689  el2xptp  30123  el2xptp0  30124  usgra2pthlem1  30297  wwlkn0  30320  wwlkn0s  30336  rusgranumwlkl1  30556  2pthfrgra  30600  mat1dimelbas  30864  lindsrng01  30999  ldepspr  31004  comraddi  31111  bnj168  31718  bnj927  31759  bnj543  31883  bnj970  31937  bj-snsetex  32453  bj-pinftynminfty  32547  cdleme25cv  33999  cdlemk35  34553  dicval2  34821  dicopelval2  34823  dicelval2N  34824  hdmap1fval  35439