Theorem eqeq1i 2427

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

Syntax hints:   <-> wb 187   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-cleq 2412

This theorem is referenced by:  eqeq12i  2440  neeq1i  2707  ssequn2  3636  dfss1  3664  dfss4  3704  disj  3830  disjr  3831  undisj1  3841  undisj2  3842  undif  3873  uneqdifeq  3881  reusn  4067  rabsneu  4069  eusn  4070  tppreqb  4135  uniintsn  4287  iin0  4590  opeqsn  4708  dfepfr  4830  epfrc  4831  dmopab3  5058  dm0rn0  5062  ssdmres  5137  imadisj  5198  args  5207  dffr3  5212  intirr  5229  dminxp  5288  dfrel3  5304  coeq0  5355  sspred  5398  dffr4  5406  tz6.26  5421  wfi  5423  unisuc  5509  fntpg  5647  fncnv  5656  mptfnf  5708  sbcfng  5734  f0rn0  5776  dff1o4  5830  dffv4  5869  fvun2  5944  fnreseql  5998  riota1  6276  riota2df  6278  fnotovb  6337  ovid  6418  ov  6421  ovg  6440  ovima0  6453  opiota  6857  wfrlem8  7042  tz7.49c  7162  sucprcreg  8105  inf3lem2  8125  zfregs2  8207  rankxpsuc  8343  scott0s  8349  cplem1  8350  cfslb2n  8687  fin23lem26  8744  dfacfin7  8818  axdc3lem4  8872  zorn2lem7  8921  alephom  8999  fpwwe2  9057  recmulnq  9378  recexsr  9520  map2psrpr  9523  renegcli  9924  elznn0  10941  xrsupss  11583  xrinfmss  11584  seqf1olem1  12238  seqf1olem2  12239  sqeqori  12372  hashrabsn1  12539  hashprb  12560  hashprdifel  12561  hashbclem  12599  hash2pwpr  12617  swrdccat3a  12824  f1oun2prg  12970  modfsummods  13820  cshwrepswhash1  15025  ismgmid  16451  oppgid  16951  lsmdisjr  17262  gexex  17419  dprd0  17592  oppr1  17790  opprunit  17817  opprdomn  18453  gsummoncoe1  18826  mat0dimcrng  19419  iinopn  19856  elcls  20013  ordthaus  20324  hauscmplem  20345  regr1lem2  20679  metdseq0  21775  minveclem1  22252  minveclem3b  22256  volun  22372  dyaddisj  22428  vieta1  23130  logeftb  23395  birthdaylem1  23739  dmgmaddn0  23810  lgseisenlem1  24137  rpvmasum  24224  axsegconlem6  24795  usgraedgprv  24946  wlkdvspthlem  25179  wlknwwlknsur  25282  wlkiswwlksur  25289  clwlkfclwwlk1hashn  25411  clwlkfoclwwlk  25415  1to3vfriswmgra  25577  frgrawopreg2  25621  rngosn3  25996  nmlno0lem  26276  minvecolem1  26358  hvsubeq0i  26548  hvsubaddi  26551  pjoc2i  26923  pjoml3i  27071  cmbr3i  27085  pjss2i  27165  hosubeq0i  27311  dmadjrnb  27391  nmlnop0iALT  27480  nmopcoadj0i  27588  stm1ri  27729  jplem2  27754  atoml2i  27868  chirredlem1  27875  cdj3lem3  27923  disjnf  28017  disjpreima  28030  disjunsn  28040  f1od2  28149  addeq0  28160  zrhchr  28616  ddemeas  28895  braew  28901  aean  28903  eulerpartlemgh  29034  ballotlemfp1  29147  bnj1143  29387  cvmsss2  29782  cvmlift2lem13  29823  elrn3  30187  br1steq  30198  br2ndeq  30199  frind  30265  sltsolem1  30339  rankeq1o  30720  hfun  30727  bj-pinftynminfty  31411  tan2h  31641  poimirlem13  31657  poimirlem14  31658  poimirlem21  31665  poimirlem22  31666  asindmre  31731  totbndbnd  31825  scott0f  32116  atbase  32564  llnbase  32783  lplnbase  32808  lvolbase  32852  lhpbase  33272  cdlemg31b0N  33970  cdlemg31b0a  33971  cdlemh  34093  iunrelexp0  35937  frege120  36220  undisjrab  36295  zfregs2VD  36881  dvnprod  37397  fnresfnco  38031  afvpcfv0  38051  aovpcov0  38095  aov0ov0  38098  aovov0bi  38101  fnotaovb  38103  usgo0s0ALT  38519  usgo1s0ALT  38520  snlindsntor  39037