Theorem eqeq1i 2448

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

Syntax hints:   <-> wb 184   = wceq 1381

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

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

This theorem is referenced by:  eqeq12i  2461  neeq1i  2726  ssequn2  3659  dfss1  3685  dfss4  3714  disj  3849  disjr  3850  undisj1  3860  undisj2  3861  undif  3890  uneqdifeq  3898  reusn  4084  rabsneu  4086  eusn  4087  tppreqb  4152  uniintsn  4305  iin0  4607  opeqsn  4729  dfepfr  4850  epfrc  4851  unisuc  4940  dmopab3  5201  dm0rn0  5205  ssdmres  5281  imadisj  5342  args  5351  dffr3  5355  intirr  5371  dminxp  5433  dfrel3  5450  coeq0  5502  fntpg  5629  fncnv  5638  sbcfng  5714  f0rn0  5756  dff1o4  5810  dffv4  5849  fvun2  5926  fnreseql  5978  riota1  6257  riota2df  6259  fnotovb  6319  ovid  6400  ov  6403  ovg  6422  ovima0  6435  opiota  6840  tz7.49c  7109  sucprcreg  8023  sucprcregOLD  8024  inf3lem2  8044  zfregs2  8162  rankxpsuc  8298  scott0s  8304  cplem1  8305  cfslb2n  8646  fin23lem26  8703  dfacfin7  8777  axdc3lem4  8831  zorn2lem7  8880  alephom  8958  fpwwe2  9019  recmulnq  9340  recexsr  9482  map2psrpr  9485  renegcli  9880  elznn0  10880  xrsupss  11504  xrinfmss  11505  seqf1olem1  12120  seqf1olem2  12121  sqeqori  12254  hashrabsn1  12416  hashprb  12436  hashprdifel  12437  hashbclem  12475  hash2pwpr  12493  swrdccat3a  12693  f1oun2prg  12839  modfsummods  13581  cshwrepswhash1  14459  ismgmid  15760  oppgid  16260  lsmdisjr  16571  gexex  16728  dprd0  16946  oppr1  17151  opprunit  17178  opprdomn  17818  gsummoncoe1  18214  mat0dimcrng  18839  iinopn  19278  elcls  19440  ordthaus  19751  hauscmplem  19772  regr1lem2  20107  metdseq0  21224  minveclem1  21705  minveclem3b  21709  volun  21821  dyaddisj  21871  vieta1  22573  logeftb  22833  birthdaylem1  23146  lgseisenlem1  23489  rpvmasum  23576  axsegconlem6  24090  usgraedgprv  24241  wlkdvspthlem  24474  wlknwwlknsur  24577  wlkiswwlksur  24584  clwlkfclwwlk1hashn  24706  clwlkfoclwwlk  24710  1to3vfriswmgra  24872  frgrawopreg2  24916  rngosn3  25293  nmlno0lem  25573  minvecolem1  25655  hvsubeq0i  25845  hvsubaddi  25848  pjoc2i  26221  pjoml3i  26369  cmbr3i  26383  pjss2i  26463  hosubeq0i  26610  dmadjrnb  26690  nmlnop0iALT  26779  nmopcoadj0i  26887  stm1ri  27028  jplem2  27053  atoml2i  27167  chirredlem1  27174  cdj3lem3  27222  disjnf  27298  disjpreima  27310  disjunsn  27318  mptfnf  27364  f1od2  27412  addeq0  27423  zrhchr  27823  ddemeas  28074  braew  28080  aean  28082  eulerpartlemgh  28183  ballotlemfp1  28296  dmgmaddn0  28431  cvmsss2  28585  cvmlift2lem13  28626  elrn3  29160  br1steq  29172  br2ndeq  29173  sspred  29220  dffr4  29230  tz6.26  29253  wfi  29255  frind  29291  wfrlem8  29318  sltsolem1  29396  rankeq1o  29796  hfun  29803  tan2h  30015  asindmre  30070  totbndbnd  30253  scott0f  30545  undisjrab  31155  fnresfnco  32045  afvpcfv0  32065  aovpcov0  32109  aov0ov0  32112  aovov0bi  32115  fnotaovb  32117  usgo0s0ALT  32270  usgo1s0ALT  32271  snlindsntor  32782  zfregs2VD  33349  bnj1143  33556  bj-pinftynminfty  34332  atbase  34716  llnbase  34935  lplnbase  34960  lvolbase  35004  lhpbase  35424  cdlemg31b0N  36122  cdlemg31b0a  36123  cdlemh  36245