Theorem eqeq2i 2438

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

Syntax hints:   <-> wb 187   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-cleq 2412

This theorem is referenced by:  eqeq12i  2440  eqtri  2449  neeq2i  2709  rabid2  3004  dfss2  3450  equncom  3608  rabrsn  4064  ssunpr  4156  sspr  4157  sstp  4158  preq12b  4170  preqsn  4177  opeqpr  4709  wefrc  4839  dfrel4v  5298  orddif  5526  dfiota2  5557  funopg  5624  funimaexg  5669  dffn5f  5927  fnressn  6082  fressnfv  6084  fnprb  6129  fnov  6409  ovmpt2s  6425  onuninsuci  6672  fvresex  6771  elxp6  6830  el2xptp  6841  el2xptp0  6842  opiota  6857  tpossym  7004  qsid  7428  mapsncnv  7517  ixpsnf1o  7561  card1  8392  pm54.43lem  8423  cf0  8670  sdom2en01  8721  cardeq0  8966  enqbreq2  9334  addcompr  9435  mulcompr  9437  axrrecex  9576  negeq0  9917  muleqadd  10245  crne0  10591  dfnn3  10612  xmulneg1  11544  hasheq0  12530  hashbc  12600  hashf1lem2  12603  hash2pwpr  12617  cjne0  13194  sqrt00  13295  sqrtmsq2i  13418  cbvsum  13728  fsump1i  13797  cbvprod  13936  bpoly2  14077  bpoly3  14078  bpoly4  14079  absefib  14219  efieq1re  14220  xpccatid  16017  isnsg4  16804  mat1dimelbas  19420  pmatcollpw3fi1lem1  19734  2ndcctbss  20394  ptcnp  20561  ovolgelb  22307  ioorinv  22402  ioorinvOLD  22407  rolle  22816  plymul0or  23099  reeff1o  23264  sineq0  23338  coseq1  23339  1cubr  23630  atandm2  23665  atandm3  23666  efrlim  23757  isppw  23901  ppiub  23992  lgsdinn0  24128  m1lgs  24150  usgra2edg  24952  usgraedg4  24957  usgraidx2vlem1  24961  usgraidx2vlem2  24962  nb3graprlem2  25022  nb3grapr  25023  nb3grapr2  25024  nb3gra2nb  25025  2trllemH  25124  2trllemE  25125  usgrcyclnl2  25211  4cycl4dv  25237  wwlkn0  25259  wwlkn0s  25275  rusgranumwlkl1  25517  2pthfrgra  25581  isgrpo  25766  vci  26009  chnlei  26970  h1de2ctlem  27040  cmcmlem  27076  cmcm2i  27078  cmbr2i  27081  osumcor2i  27129  pjss2i  27165  ho01i  27313  nmop0h  27476  pjclem1  27680  jplem1  27753  atabs2i  27887  rabid2f  27969  preqsnd  27993  dfrel4  28044  bnj168  29323  bnj927  29365  bnj543  29489  bnj970  29543  subfacp1lem6  29693  mppspstlem  29994  quad3  30087  trpredmintr  30256  brdomain  30482  brrange  30483  brimg  30486  brapply  30487  brsuccf  30490  brfullfun  30497  brrestrict  30498  rankeq1o  30720  bj-snsetex  31303  bj-pinftynminfty  31411  ismblfin  31685  opropabco  31754  fdc  31778  isdrngo1  31899  smprngopr  31989  cdleme25cv  33634  cdlemk35  34188  dicval2  34456  dicopelval2  34458  dicelval2N  34459  hdmap1fval  35074  mzpcompact2lem  35302  eldioph4b  35363  2nn0ind  35503  islmodfg  35637  brtrclfv2  35962  frege116  36216  elnev  36430  dvnprodlem1  37394  fourierdlem103  37645  fourierdlem104  37646  usgra2pthlem1  38436  usgedgvadf1lem1  38496  usgedgvadf1lem2  38497  usgedgvadf1ALTlem1  38499  usgedgvadf1ALTlem2  38500  lindsrng01  39034  ldepspr  39039  nn0sumshdiglemB  39205