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 1398

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

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

This theorem is referenced by:  eqeq12i  2474  neeq1i  2739  ssequn2  3663  dfss1  3689  dfss4  3729  disj  3855  disjr  3856  undisj1  3866  undisj2  3867  undif  3896  uneqdifeq  3904  reusn  4089  rabsneu  4091  eusn  4092  tppreqb  4157  uniintsn  4309  iin0  4611  opeqsn  4732  dfepfr  4853  epfrc  4854  unisuc  4943  dmopab3  5204  dm0rn0  5208  ssdmres  5283  imadisj  5344  args  5353  dffr3  5357  intirr  5373  dminxp  5432  dfrel3  5448  coeq0  5499  fntpg  5625  fncnv  5634  sbcfng  5710  f0rn0  5752  dff1o4  5806  dffv4  5845  fvun2  5920  fnreseql  5973  riota1  6250  riota2df  6252  fnotovb  6311  ovid  6392  ov  6395  ovg  6414  ovima0  6427  opiota  6832  tz7.49c  7103  sucprcreg  8017  inf3lem2  8037  zfregs2  8155  rankxpsuc  8291  scott0s  8297  cplem1  8298  cfslb2n  8639  fin23lem26  8696  dfacfin7  8770  axdc3lem4  8824  zorn2lem7  8873  alephom  8951  fpwwe2  9010  recmulnq  9331  recexsr  9473  map2psrpr  9476  renegcli  9871  elznn0  10875  xrsupss  11503  xrinfmss  11504  seqf1olem1  12128  seqf1olem2  12129  sqeqori  12262  hashrabsn1  12425  hashprb  12446  hashprdifel  12447  hashbclem  12485  hash2pwpr  12503  swrdccat3a  12710  f1oun2prg  12856  modfsummods  13689  cshwrepswhash1  14671  ismgmid  16090  oppgid  16590  lsmdisjr  16901  gexex  17058  dprd0  17273  oppr1  17478  opprunit  17505  opprdomn  18145  gsummoncoe1  18541  mat0dimcrng  19139  iinopn  19578  elcls  19741  ordthaus  20052  hauscmplem  20073  regr1lem2  20407  metdseq0  21524  minveclem1  22005  minveclem3b  22009  volun  22121  dyaddisj  22171  vieta1  22874  logeftb  23137  birthdaylem1  23479  lgseisenlem1  23822  rpvmasum  23909  axsegconlem6  24427  usgraedgprv  24578  wlkdvspthlem  24811  wlknwwlknsur  24914  wlkiswwlksur  24921  clwlkfclwwlk1hashn  25043  clwlkfoclwwlk  25047  1to3vfriswmgra  25209  frgrawopreg2  25253  rngosn3  25626  nmlno0lem  25906  minvecolem1  25988  hvsubeq0i  26178  hvsubaddi  26181  pjoc2i  26554  pjoml3i  26702  cmbr3i  26716  pjss2i  26796  hosubeq0i  26943  dmadjrnb  27023  nmlnop0iALT  27112  nmopcoadj0i  27220  stm1ri  27361  jplem2  27386  atoml2i  27500  chirredlem1  27507  cdj3lem3  27555  disjnf  27643  disjpreima  27655  disjunsn  27664  mptfnf  27721  f1od2  27778  addeq0  27789  zrhchr  28191  ddemeas  28445  braew  28451  aean  28453  eulerpartlemgh  28581  ballotlemfp1  28694  dmgmaddn0  28829  cvmsss2  28983  cvmlift2lem13  29024  elrn3  29433  br1steq  29444  br2ndeq  29445  sspred  29492  dffr4  29502  tz6.26  29525  wfi  29527  frind  29563  wfrlem8  29590  sltsolem1  29668  rankeq1o  30056  hfun  30063  tan2h  30287  asindmre  30342  totbndbnd  30525  scott0f  30817  undisjrab  31427  dvnprod  31985  fnresfnco  32450  afvpcfv0  32470  aovpcov0  32514  aov0ov0  32517  aovov0bi  32520  fnotaovb  32522  usgo0s0ALT  32808  usgo1s0ALT  32809  snlindsntor  33326  zfregs2VD  34041  bnj1143  34250  bj-pinftynminfty  35030  atbase  35411  llnbase  35630  lplnbase  35655  lvolbase  35699  lhpbase  36119  cdlemg31b0N  36817  cdlemg31b0a  36818  cdlemh  36940  iunrelexp0  38224