Theorem eqeq1i 2456

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

Syntax hints:   <-> wb 188   = wceq 1444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-cleq 2444

This theorem is referenced by:  eqeq12i  2465  neeq1i  2688  ssequn2  3607  dfss1  3637  dfss4  3677  disj  3805  disjr  3806  undisj1  3816  undisj2  3817  undif  3848  uneqdifeq  3856  reusn  4045  rabsneu  4047  eusn  4048  tppreqb  4113  elpreqpr  4161  uniintsn  4272  iin0  4577  opeqsn  4697  dfepfr  4819  epfrc  4820  dmopab3  5047  dm0rn0  5051  ssdmres  5126  imadisj  5187  args  5196  dffr3  5201  intirr  5218  dminxp  5277  dfrel3  5293  coeq0  5344  sspred  5388  dffr4  5396  tz6.26  5411  wfi  5413  unisuc  5499  fntpg  5637  fncnv  5647  mptfnf  5699  sbcfng  5725  f0rn0  5768  dff1o4  5822  dffv4  5862  fvun2  5937  fnreseql  5992  riota1  6270  riota2df  6272  fnotovb  6331  ovid  6413  ov  6416  ovg  6435  ovima0  6448  opiota  6852  wfrlem8  7043  tz7.49c  7163  sucprcreg  8114  inf3lem2  8134  zfregs2  8217  rankxpsuc  8353  scott0s  8359  cplem1  8360  cfslb2n  8698  fin23lem26  8755  dfacfin7  8829  axdc3lem4  8883  zorn2lem7  8932  alephom  9010  fpwwe2  9068  recmulnq  9389  recexsr  9531  map2psrpr  9534  renegcli  9935  elznn0  10952  xrsupss  11594  xrinfmss  11595  seqf1olem1  12252  seqf1olem2  12253  sqeqori  12386  hashrabsn1  12553  hashprb  12574  hashprdifel  12575  hashbclem  12615  hash2pwpr  12635  swrdccat3a  12850  f1oun2prg  13002  modfsummods  13853  cshwrepswhash1  15073  ismgmid  16507  oppgid  17007  lsmdisjr  17334  gexex  17491  dprd0  17664  oppr1  17862  opprunit  17889  opprdomn  18525  gsummoncoe1  18898  mat0dimcrng  19495  iinopn  19932  elcls  20089  ordthaus  20400  hauscmplem  20421  regr1lem2  20755  metdseq0  21871  metdseq0OLD  21886  minveclem1  22366  minveclem3b  22370  minveclem3bOLD  22382  volun  22498  dyaddisj  22554  vieta1  23265  logeftb  23533  birthdaylem1  23877  dmgmaddn0  23948  lgseisenlem1  24277  rpvmasum  24364  axsegconlem6  24952  usgraedgprv  25103  wlkdvspthlem  25337  wlknwwlknsur  25440  wlkiswwlksur  25447  clwlkfclwwlk1hashn  25569  clwlkfoclwwlk  25573  1to3vfriswmgra  25735  frgrawopreg2  25779  rngosn3  26154  nmlno0lem  26434  minvecolem1  26516  hvsubeq0i  26716  hvsubaddi  26719  pjoc2i  27091  pjoml3i  27239  cmbr3i  27253  pjss2i  27333  hosubeq0i  27479  dmadjrnb  27559  nmlnop0iALT  27648  nmopcoadj0i  27756  stm1ri  27897  jplem2  27922  atoml2i  28036  chirredlem1  28043  cdj3lem3  28091  disjnf  28181  disjpreima  28194  disjunsn  28204  f1od2  28309  addeq0  28320  zrhchr  28780  ddemeas  29059  braew  29065  aean  29067  eulerpartlemgh  29211  ballotlemfp1  29324  bnj1143  29602  cvmsss2  29997  cvmlift2lem13  30038  elrn3  30403  br1steq  30414  br2ndeq  30415  frind  30481  sltsolem1  30557  rankeq1o  30938  hfun  30945  bj-pinftynminfty  31669  finxpreclem4  31786  tan2h  31937  poimirlem13  31953  poimirlem14  31954  poimirlem21  31961  poimirlem22  31962  asindmre  32027  totbndbnd  32121  scott0f  32412  atbase  32855  llnbase  33074  lplnbase  33099  lvolbase  33143  lhpbase  33563  cdlemg31b0N  34261  cdlemg31b0a  34262  cdlemh  34384  iunrelexp0  36294  frege120  36579  undisjrab  36654  zfregs2VD  37237  dvnprod  37824  fnresfnco  38627  afvpcfv0  38648  aovpcov0  38692  aov0ov0  38695  aovov0bi  38698  fnotaovb  38700  riotaeqimp  39037  prinfzo0  39066  ushgredgedga  39306  ushgredgedgaloop  39308  uhgr0v0e  39314  usgrexmpllem  39332  usgr1v0e  39392  nbuhgr2vtx1edgblem  39419  uvtxa01vtx0  39469  uvtxa01vtx  39470  cusgr0v  39496  vtxdg0e  39534  uspgrloopvd2  39557  isrgr  39577  fusgrregdegfi  39586  usgo0s0ALT  39801  usgo1s0ALT  39802  snlindsntor  40317