Theorem eqeq1i 2461

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

Syntax hints:   <-> wb 184   = wceq 1370

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

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

This theorem is referenced by:  eqeq12i  2474  neeq1i  2736  ssequn2  3636  dfss1  3662  dfss4  3691  disj  3826  disjr  3827  undisj1  3837  undisj2  3838  undif  3866  uneqdifeq  3874  reusn  4055  rabsneu  4057  eusn  4058  tppreqb  4121  uniintsn  4272  iin0  4573  opeqsn  4694  dfepfr  4812  epfrc  4813  unisuc  4902  dmopab3  5159  dm0rn0  5163  ssdmres  5239  imadisj  5295  args  5304  dffr3  5308  intirr  5323  dminxp  5385  dfrel3  5402  fntpg  5580  fncnv  5589  sbcfng  5663  dff1o4  5756  dffv4  5795  fvun2  5871  fnreseql  5921  riota1  6179  riota2df  6181  fnotovb  6237  ovid  6316  ov  6319  ovg  6338  ovima0  6351  opiota  6742  tz7.49c  7010  sucprcreg  7924  sucprcregOLD  7925  inf3lem2  7945  zfregs2  8063  rankxpsuc  8199  scott0s  8205  cplem1  8206  cfslb2n  8547  fin23lem26  8604  dfacfin7  8678  axdc3lem4  8732  zorn2lem7  8781  alephom  8859  fpwwe2  8920  recmulnq  9243  recexsr  9384  map2psrpr  9387  renegcli  9780  elznn0  10771  xrsupss  11381  xrinfmss  11382  seqf1olem1  11961  seqf1olem2  11962  sqeqori  12094  hashprb  12274  hash2pwpr  12299  hashbclem  12322  swrdccat3a  12502  f1oun2prg  12644  cshwrepswhash1  14246  ismgmid  15553  oppgid  15989  lsmdisjr  16301  gexex  16455  dprd0  16649  oppr1  16848  opprunit  16875  opprdomn  17495  iinopn  18646  elcls  18808  ordthaus  19119  hauscmplem  19140  regr1lem2  19444  metdseq0  20561  minveclem1  21042  minveclem3b  21046  volun  21158  dyaddisj  21208  vieta1  21910  logeftb  22164  birthdaylem1  22477  lgseisenlem1  22820  rpvmasum  22907  axsegconlem6  23319  usgraedgprv  23446  wlkdvspthlem  23657  rngosn3  24064  nmlno0lem  24344  minvecolem1  24426  hvsubeq0i  24616  hvsubaddi  24619  pjoc2i  24992  pjoml3i  25140  cmbr3i  25154  pjss2i  25234  hosubeq0i  25381  dmadjrnb  25461  nmlnop0iALT  25550  nmopcoadj0i  25658  stm1ri  25799  jplem2  25824  atoml2i  25938  chirredlem1  25945  cdj3lem3  25993  disjnf  26066  disjpreima  26078  disjunsn  26086  mptfnf  26126  f1od2  26174  addeq0  26185  zrhchr  26549  ddemeas  26795  braew  26801  aean  26803  eulerpartgbij  26898  eulerpartlemgh  26904  fib5  26931  fib6  26932  ballotlemfp1  27017  dmgmaddn0  27152  cvmsss2  27306  cvmlift2lem13  27347  elrn3  27716  br1steq  27728  br2ndeq  27729  sspred  27776  dffr4  27786  tz6.26  27809  wfi  27811  frind  27847  wfrlem8  27874  sltsolem1  27952  rankeq1o  28352  hfun  28359  tan2h  28571  asindmre  28626  totbndbnd  28835  scott0f  29128  coeq0  29237  fnresfnco  30179  afvpcfv0  30199  aovpcov0  30243  aov0ov0  30246  aovov0bi  30249  fnotaovb  30251  f0rn0  30288  hashrabsn1  30380  modfsummods  30391  wlknwwlknsur  30491  wlkiswwlksur  30498  clwlkfclwwlk1hashn  30661  clwlkfoclwwlk  30665  1to3vfriswmgra  30746  frgrawopreg2  30791  gsummoncoe1  30995  mat0dimcrng  31031  snlindsntor  31123  zfregs2VD  31894  bnj1143  32101  bj-pinftynminfty  32873  atbase  33257  llnbase  33476  lplnbase  33501  lvolbase  33545  lhpbase  33965  cdlemg31b0N  34661  cdlemg31b0a  34662  cdlemh  34784