Theorem eqeq1i 2445

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

Syntax hints:   <-> wb 184   = wceq 1369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2431

This theorem is referenced by:  ssequn2  3524  dfss1  3550  dfss4  3579  disj  3714  disjr  3715  undisj1  3725  undisj2  3726  undif  3754  uneqdifeq  3762  reusn  3943  rabsneu  3945  eusn  3946  tppreqb  4009  uniintsn  4160  iin0  4461  opeqsn  4582  dfepfr  4700  epfrc  4701  unisuc  4790  dmopab3  5047  dm0rn0  5051  ssdmres  5127  imadisj  5183  args  5192  dffr3  5196  intirr  5211  dminxp  5273  dfrel3  5290  fntpg  5468  fncnv  5477  sbcfng  5551  dff1o4  5644  dffv4  5683  fvun2  5758  fnreseql  5808  riota1  6066  riota2df  6068  fnotovb  6124  ovid  6202  ov  6205  ovg  6224  ovima0  6237  opiota  6628  tz7.49c  6893  sucprcreg  7806  sucprcregOLD  7807  inf3lem2  7827  zfregs2  7945  rankxpsuc  8081  scott0s  8087  cplem1  8088  cfslb2n  8429  fin23lem26  8486  dfacfin7  8560  axdc3lem4  8614  zorn2lem7  8663  alephom  8741  fpwwe2  8802  recmulnq  9125  recexsr  9266  map2psrpr  9269  renegcli  9662  elznn0  10653  xrsupss  11263  xrinfmss  11264  seqf1olem1  11837  seqf1olem2  11838  sqeqori  11970  hashprb  12149  hash2pwpr  12174  hashbclem  12197  swrdccat3a  12377  f1oun2prg  12519  cshwrepswhash1  14121  ismgmid  15427  oppgid  15862  lsmdisjr  16172  gexex  16326  dprd0  16516  oppr1  16714  opprunit  16741  opprdomn  17350  iinopn  18490  elcls  18652  ordthaus  18963  hauscmplem  18984  regr1lem2  19288  metdseq0  20405  minveclem1  20886  minveclem3b  20890  volun  21001  dyaddisj  21051  vieta1  21753  logeftb  22007  birthdaylem1  22320  lgseisenlem1  22663  rpvmasum  22750  axsegconlem6  23119  usgraedgprv  23246  wlkdvspthlem  23457  rngosn3  23864  nmlno0lem  24144  minvecolem1  24226  hvsubeq0i  24416  hvsubaddi  24419  pjoc2i  24792  pjoml3i  24940  cmbr3i  24954  pjss2i  25034  hosubeq0i  25181  dmadjrnb  25261  nmlnop0iALT  25350  nmopcoadj0i  25458  stm1ri  25599  jplem2  25624  atoml2i  25738  chirredlem1  25745  cdj3lem3  25793  disjnf  25867  disjpreima  25879  disjunsn  25887  mptfnf  25927  f1od2  25975  addeq0  25986  zrhchr  26357  ddemeas  26604  braew  26610  aean  26612  eulerpartgbij  26707  eulerpartlemgh  26713  fib5  26740  fib6  26741  ballotlemfp1  26826  dmgmaddn0  26961  cvmsss2  27115  cvmlift2lem13  27156  elrn3  27524  br1steq  27536  br2ndeq  27537  sspred  27584  dffr4  27594  tz6.26  27617  wfi  27619  frind  27655  wfrlem8  27682  sltsolem1  27760  rankeq1o  28160  hfun  28167  tan2h  28377  asindmre  28432  totbndbnd  28641  scott0f  28934  coeq0  29043  fnresfnco  29985  afvpcfv0  30005  aovpcov0  30049  aov0ov0  30052  aovov0bi  30055  fnotaovb  30057  f0rn0  30094  hashrabsn1  30186  modfsummods  30197  wlknwwlknsur  30297  wlkiswwlksur  30304  clwlkfclwwlk1hashn  30467  clwlkfoclwwlk  30471  1to3vfriswmgra  30552  frgrawopreg2  30597  mat0dimcrng  30789  snlindsntor  30894  zfregs2VD  31464  bnj1143  31671  bj-pinftynminfty  32397  atbase  32774  llnbase  32993  lplnbase  33018  lvolbase  33062  lhpbase  33482  cdlemg31b0N  34178  cdlemg31b0a  34179  cdlemh  34301