Theorem eqeq1i 2739

Description: Inference from equality to equivalence of equalities. (Contributed by NM, 15-Jul-1993.)

Hypothesis

Ref	Expression
eqeq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqeq1i	⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Proof of Theorem eqeq1i

Step	Hyp	Ref	Expression
1		eqeq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eqeq1 2738	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726

This theorem is referenced by:  eqeq12i  2752  eqabb  2873  neeq1i  2995  dfss2  3942  ssequn2  4162  ineqcom  4183  sseqin2  4196  dfss7  4224  dfss4  4242  rabeq0w  4360  rabeq0  4361  disj  4423  disjr  4424  undisj1  4435  undisj2  4436  undif  4455  undifr  4456  undifrOLD  4457  uneqdifeq  4466  rabeqsn  4640  reusn  4700  rabsneu  4702  eusn  4703  tppreqb  4778  elpreqpr  4840  uniintsn  4958  iin0  5329  dfepfr  5635  epfrc  5636  dmopab3  5896  dm0rn0  5901  rnopab3  5933  ssdmres  5997  iresn0n0  6038  imadisj  6064  args  6076  dffr3  6083  intirr  6104  dminxp  6166  dfrel3  6184  coeq0  6241  snres0  6284  sspred  6296  dffr4  6306  frpomin2  6327  frpoind  6328  tz6.26OLD  6334  wfiOLD  6337  cbviotavw  6488  fntpg  6592  fncnv  6605  mptfnf  6669  sbcfng  6699  f0rn0  6759  dff1o4  6822  dffv4  6869  tz6.12c  6894  fvun2  6967  fnreseql  7034  funopdmsn  7136  riota1  7377  riota2df  7379  riotaeqimp  7382  fnbrovb  7450  ovid  7542  ov  7545  ovg  7566  ovima0  7580  opiota  8052  frrlem13  8291  wfrlem8OLD  8324  tz7.49c  8454  sucprcreg  9607  zfregfr  9611  inf3lem2  9635  zfregs2  9739  frind  9756  rankxpsuc  9888  scott0s  9894  cplem1  9895  cfslb2n  10274  fin23lem26  10331  dfacfin7  10405  axdc3lem4  10459  zorn2lem7  10508  alephom  10591  fpwwe2  10649  recmulnq  10970  recexsr  11113  map2psrpr  11116  renegcli  11536  addeq0  11652  elznn0  12595  xrsupss  13317  xrinfmss  13318  prinfzo0  13704  seqf1olem1  14048  seqf1olem2  14049  sqeqori  14220  hashrabsn1  14380  hashprb  14403  hashprdifel  14404  hashbclem  14458  hash2pwpr  14482  f1oun2prg  14923  modfsummods  15796  cshwrepswhash1  17107  ismgmid  18628  smndex2dnrinv  18878  oppgid  19324  lsmdisjr  19650  gexex  19819  gsumxp2  19946  dprd0  19999  oppr1  20295  opprunit  20322  zringndrg  21414  gsummoncoe1  22231  mat0dimcrng  22393  iinopn  22825  elcls  22996  ordthaus  23307  hauscmplem  23329  regr1lem2  23663  metdseq0  24779  minveclem1  25361  minveclem3b  25365  volun  25483  dyaddisj  25534  vieta1  26257  logeftb  26528  birthdaylem1  26897  dmgmaddn0  26969  gausslemma2d  27321  lgseisenlem1  27322  2lgslem4  27353  rpvmasum  27473  sltsolem1  27623  noinfbnd2lem1  27678  madeval2  27795  made0  27815  axsegconlem6  28833  edg0iedg0  28966  numedglnl  29055  ushgredgedg  29140  ushgredgedgloop  29142  uhgr0v0e  29149  usgr1v0edg  29168  usgrexmpllem  29171  usgr1v0e  29237  nbuhgr2vtx1edgblem  29262  uvtx01vtx  29308  prcliscplgr  29325  cusgr0v  29339  vtxdg0e  29386  1loopgrvd2  29415  finsumvtxdg2ssteplem4  29460  finsumvtxdg2size  29462  isrgr  29471  fusgrregdegfi  29481  wspn0  29838  2wlkdlem8  29847  3wlkdlem8  30080  uhgr3cyclexlem  30094  1to2vfriswmgr  30192  1to3vfriswmgr  30193  frgrregorufr0  30237  frgrreg  30307  frgrregord013  30308  ex-ceil  30361  nmlno0lem  30706  minvecolem1  30787  hvsubeq0i  30976  hvsubaddi  30979  pjoc2i  31351  pjoml3i  31499  cmbr3i  31513  pjss2i  31593  hosubeq0i  31739  dmadjrnb  31819  nmlnop0iALT  31908  nmopcoadj0i  32016  stm1ri  32157  jplem2  32182  atoml2i  32296  chirredlem1  32303  cdj3lem3  32351  difininv  32430  disjnf  32484  disjpreima  32498  disjunsn  32508  f1od2  32633  wrdt2ind  32848  isunit2  33153  isdrng4  33207  lsmsnorb2  33325  ssdifidlprm  33391  fldext2chn  33678  zrhchr  33913  ddemeas  34175  braew  34181  aean  34183  eulerpartlemgh  34318  ballotlemfp1  34432  repr0  34564  hgt750lem2  34605  bnj1143  34742  nummin  35043  acycgr0v  35091  prclisacycgr  35094  cvmsss2  35217  cvmlift2lem13  35258  elrn3  35700  rankeq1o  36110  hfun  36117  bj-disj2r  36967  bj-sscon  36968  bj-0int  37040  bj-imdirco  37129  bj-pinftynminfty  37166  finxpreclem4  37333  nlpineqsn  37347  curunc  37547  tan2h  37557  poimirlem13  37578  poimirlem14  37579  poimirlem21  37586  poimirlem22  37587  asindmre  37648  totbndbnd  37734  rngosn3  37869  scott0f  38114  n0el2  38272  dfrel5  38285  dfrel6  38286  redundeq1  38568  dmqscoelseq  38600  dfeldisj5  38660  atbase  39228  llnbase  39449  lplnbase  39474  lvolbase  39518  lhpbase  39938  cdlemg31b0N  40634  cdlemg31b0a  40635  cdlemh  40757  sticksstones16  42097  sticksstones21  42102  unitscyglem3  42132  metakunt24  42163  onsupmaxb  43188  iunrelexp0  43651  frege120  43932  clsk1indlem4  43993  gneispace  44083  scotteld  44196  undisjrab  44256  zfregs2VD  44792  dvnprod  45908  fnresfnco  46998  aiotavb  47047  afvpcfv0  47103  aovpcov0  47147  aov0ov0  47150  aovov0bi  47153  fnotaovb  47155  funressndmafv2rn  47180  fmtnoprmfac1lem  47496  lighneallem2  47538  stgrvtx0  47874  isubgr3stgrlem6  47883  snlindsntor  48333  rrx2pnedifcoorneorr  48583  itschlc0xyqsol1  48632  2itscp  48647  resinsn  48727  resinsnALT  48728  opndisj  48756  istermc  49145