Theorem eqeq1i 2476

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	|- A = B

Assertion

Ref	Expression
eqeq1i	|- ( A = C <-> B = C )

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 |- A = B
2		eqeq1 2475	. 2 |- ( A = B -> ( A = C <-> B = C ) )
3	1, 2	ax-mp 5	1 |- ( A = C <-> B = C )

Syntax hints:   <-> wb 189   = wceq 1452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-cleq 2464

This theorem is referenced by:  eqeq12i  2485  neeq1i  2707  ssequn2  3598  dfss1  3628  dfss4  3668  disj  3809  disjr  3810  undisj1  3820  undisj2  3821  undif  3839  uneqdifeq  3847  reusn  4036  rabsneu  4038  eusn  4039  tppreqb  4104  elpreqpr  4153  uniintsn  4263  iin0  4575  opeqsn  4697  dfepfr  4824  epfrc  4825  dmopab3  5053  dm0rn0  5057  ssdmres  5132  imadisj  5193  args  5202  dffr3  5207  intirr  5224  dminxp  5283  dfrel3  5300  coeq0  5351  sspred  5395  dffr4  5403  tz6.26  5418  wfi  5420  unisuc  5506  fntpg  5644  fncnv  5657  mptfnf  5709  sbcfng  5736  f0rn0  5781  dff1o4  5836  dffv4  5876  fvun2  5952  fnreseql  6007  riota1  6288  riota2df  6290  fnotovb  6349  ovid  6432  ov  6435  ovg  6454  ovima0  6467  opiota  6871  wfrlem8  7061  tz7.49c  7181  sucprcreg  8132  inf3lem2  8152  zfregs2  8235  rankxpsuc  8371  scott0s  8377  cplem1  8378  cfslb2n  8716  fin23lem26  8773  dfacfin7  8847  axdc3lem4  8901  zorn2lem7  8950  alephom  9028  fpwwe2  9086  recmulnq  9407  recexsr  9549  map2psrpr  9552  renegcli  9955  elznn0  10976  xrsupss  11619  xrinfmss  11620  seqf1olem1  12290  seqf1olem2  12291  sqeqori  12424  hashrabsn1  12591  hashprb  12612  hashprdifel  12613  hashbclem  12656  hash2pwpr  12676  swrdccat3a  12904  f1oun2prg  13071  modfsummods  13930  cshwrepswhash1  15151  ismgmid  16585  oppgid  17085  lsmdisjr  17412  gexex  17569  dprd0  17742  oppr1  17940  opprunit  17967  opprdomn  18602  gsummoncoe1  18975  mat0dimcrng  19572  iinopn  20009  elcls  20166  ordthaus  20477  hauscmplem  20498  regr1lem2  20832  metdseq0  21949  metdseq0OLD  21964  minveclem1  22444  minveclem3b  22448  minveclem3bOLD  22460  volun  22577  dyaddisj  22633  vieta1  23344  logeftb  23612  birthdaylem1  23956  dmgmaddn0  24027  lgseisenlem1  24356  rpvmasum  24443  axsegconlem6  25031  usgraedgprv  25182  wlkdvspthlem  25416  wlknwwlknsur  25519  wlkiswwlksur  25526  clwlkfclwwlk1hashn  25648  clwlkfoclwwlk  25652  1to3vfriswmgra  25814  frgrawopreg2  25858  rngosn3  26235  nmlno0lem  26515  minvecolem1  26597  hvsubeq0i  26797  hvsubaddi  26800  pjoc2i  27172  pjoml3i  27320  cmbr3i  27334  pjss2i  27414  hosubeq0i  27560  dmadjrnb  27640  nmlnop0iALT  27729  nmopcoadj0i  27837  stm1ri  27978  jplem2  28003  atoml2i  28117  chirredlem1  28124  cdj3lem3  28172  disjnf  28258  disjpreima  28271  disjunsn  28281  f1od2  28384  addeq0  28395  zrhchr  28854  ddemeas  29132  braew  29138  aean  29140  eulerpartlemgh  29284  ballotlemfp1  29397  bnj1143  29674  cvmsss2  30069  cvmlift2lem13  30110  elrn3  30474  br1steq  30485  br2ndeq  30486  frind  30552  sltsolem1  30628  rankeq1o  31009  hfun  31016  bj-pinftynminfty  31739  finxpreclem4  31856  tan2h  32001  poimirlem13  32017  poimirlem14  32018  poimirlem21  32025  poimirlem22  32026  asindmre  32091  totbndbnd  32185  scott0f  32476  atbase  32926  llnbase  33145  lplnbase  33170  lvolbase  33214  lhpbase  33634  cdlemg31b0N  34332  cdlemg31b0a  34333  cdlemh  34455  iunrelexp0  36365  frege120  36650  undisjrab  36724  zfregs2VD  37300  dvnprod  37921  fnresfnco  38772  afvpcfv0  38793  aovpcov0  38837  aov0ov0  38840  aovov0bi  38843  fnotaovb  38845  riotaeqimp  39183  prinfzo0  39211  ushgredgedga  39470  ushgredgedgaloop  39472  uhgr0v0e  39478  usgrexmpllem  39496  usgr1v0e  39556  nbuhgr2vtx1edgblem  39583  uvtxa01vtx0  39633  uvtxa01vtx  39634  cusgr0v  39660  vtxdg0e  39699  1loopgrvd2  39725  isrgr  39766  fusgrregdegfi  39775  21wlkdlem8  40055  31wlkdlem8  40081  uhgr3cyclexlem  40095  usgo0s0ALT  40256  usgo1s0ALT  40257  snlindsntor  40772