Theorem eqeq2i 2634

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

Syntax hints:   <-> wb 196   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  eqeq12i  2636  eqtri  2644  neeq2i  2859  rabid2  3118  rabid2f  3119  dfss2  3591  equncom  3758  rabrsn  4259  ssunpr  4365  sspr  4366  sstp  4367  preq12b  4382  preqsnd  4392  preqsn  4393  preqsnOLD  4394  opeqpr  4968  propssopi  4971  wefrc  5108  dfrel4v  5584  dfrel4  5585  orddif  5820  dfiota2  5852  funopg  5922  funimaexg  5975  funcocnv2  6161  dffn5f  6252  fnressn  6425  fressnfv  6427  fnprb  6472  fntpb  6473  riotaeqimp  6634  fnov  6768  ovmpt2s  6784  onuninsuci  7040  fvresex  7139  elxp6  7200  el2xptp  7211  el2xptp0  7212  opiota  7229  tpossym  7384  qsid  7813  mapsncnv  7904  ixpsnf1o  7948  card1  8794  pm54.43lem  8825  cf0  9073  sdom2en01  9124  cardeq0  9374  enqbreq2  9742  addcompr  9843  mulcompr  9845  axrrecex  9984  negeq0  10335  muleqadd  10671  crne0  11013  dfnn3  11034  xmulneg1  12099  hasheq0  13154  hashbc  13237  hashf1lem2  13240  hash2pwpr  13258  eqwrds3  13704  cjne0  13903  sqrt00  14004  sqrtmsq2i  14127  cbvsum  14425  fsump1i  14500  cbvprod  14645  bpoly2  14788  bpoly3  14789  bpoly4  14790  absefib  14928  efieq1re  14929  xpccatid  16828  isnsg4  17637  mat1dimelbas  20277  pmatcollpw3fi1lem1  20591  2ndcctbss  21258  ptcnp  21425  ovolgelb  23248  ioorinv  23344  rolle  23753  plymul0or  24036  reeff1o  24201  sineq0  24273  coseq1  24274  1cubr  24569  atandm2  24604  atandm3  24605  efrlim  24696  isppw  24840  ppiub  24929  lgsdinn0  25070  m1lgs  25113  uhgr2edg  26100  usgredg2vlem1  26117  usgredg2vlem2  26118  ushgredgedg  26121  ushgredgedgloop  26123  edgnbusgreu  26269  nb3grprlem2  26283  nb3gr2nb  26286  usgredgsscusgredg  26355  usgr2wlkneq  26652  usgr2pthlem  26659  crctcshwlkn0  26713  wwlksn0s  26746  umgr2adedgwlk  26841  umgr2adedgspth  26844  elwwlks2ons3  26848  elwwlks2s3  26859  rusgrnumwwlkl1  26863  frgr3v  27139  frgrregorufr0  27188  isgrpo  27351  vciOLD  27416  chnlei  28344  h1de2ctlem  28414  cmcmlem  28450  cmcm2i  28452  cmbr2i  28455  osumcor2i  28503  pjss2i  28539  ho01i  28687  nmop0h  28850  pjclem1  29054  jplem1  29127  atabs2i  29261  breprexp  30711  bnj168  30798  bnj927  30839  bnj543  30963  bnj970  31017  subfacp1lem6  31167  mppspstlem  31468  quad3  31564  trpredmintr  31731  brdomain  32040  brrange  32041  brimg  32044  brapply  32045  brsuccf  32048  brfullfun  32055  brrestrict  32056  rankeq1o  32278  bj-snsetex  32951  bj-rest10  33041  bj-pinftynminfty  33114  dffinxpf  33222  finxp0  33228  matunitlindflem1  33405  ismblfin  33450  opropabco  33518  fdc  33541  isdrngo1  33755  smprngopr  33851  cdleme25cv  35646  cdlemk35  36200  dicval2  36468  dicopelval2  36470  dicelval2N  36471  hdmap1fval  37086  mzpcompact2lem  37314  eldioph4b  37375  2nn0ind  37510  islmodfg  37639  relintab  37889  brtrclfv2  38019  frege116  38273  elnev  38639  dvnprodlem1  40161  fourierdlem103  40426  fourierdlem104  40427  ovnovollem3  40872  fmtno4prmfac  41484  lindsrng01  42257  ldepspr  42262  nn0sumshdiglemB  42414