Theorem eqeq1i 2740

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 2739	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727

This theorem is referenced by:  eqeq12i  2753  eqabb  2874  neeq1i  2996  dfss2  3944  ssequn2  4164  ineqcom  4185  sseqin2  4198  dfss7  4226  dfss4  4244  rabeq0w  4362  rabeq0  4363  disj  4425  disjr  4426  undisj1  4437  undisj2  4438  undif  4457  undifr  4458  undifrOLD  4459  uneqdifeq  4468  rabeqsn  4643  reusn  4703  rabsneu  4705  eusn  4706  tppreqb  4781  elpreqpr  4843  uniintsn  4961  iin0  5332  dfepfr  5638  epfrc  5639  dmopab3  5899  dm0rn0  5904  rnopab3  5936  ssdmres  6000  iresn0n0  6041  imadisj  6067  args  6079  dffr3  6086  intirr  6107  dminxp  6169  dfrel3  6187  coeq0  6244  snres0  6287  sspred  6299  dffr4  6309  frpomin2  6330  frpoind  6331  tz6.26OLD  6337  wfiOLD  6340  cbviotavw  6491  fntpg  6595  fncnv  6608  mptfnf  6672  sbcfng  6702  f0rn0  6762  dff1o4  6825  dffv4  6872  tz6.12c  6897  fvun2  6970  fnreseql  7037  funopdmsn  7139  riota1  7381  riota2df  7383  riotaeqimp  7386  fnbrovb  7454  ovid  7546  ov  7549  ovg  7570  ovima0  7584  opiota  8056  frrlem13  8295  wfrlem8OLD  8328  tz7.49c  8458  sucprcreg  9613  zfregfr  9617  inf3lem2  9641  zfregs2  9745  frind  9762  rankxpsuc  9894  scott0s  9900  cplem1  9901  cfslb2n  10280  fin23lem26  10337  dfacfin7  10411  axdc3lem4  10465  zorn2lem7  10514  alephom  10597  fpwwe2  10655  recmulnq  10976  recexsr  11119  map2psrpr  11122  renegcli  11542  addeq0  11658  elznn0  12601  xrsupss  13323  xrinfmss  13324  prinfzo0  13713  seqf1olem1  14057  seqf1olem2  14058  sqeqori  14230  hashrabsn1  14390  hashprb  14413  hashprdifel  14414  hashbclem  14468  hash2pwpr  14492  f1oun2prg  14934  modfsummods  15807  cshwrepswhash1  17120  ismgmid  18641  smndex2dnrinv  18891  oppgid  19337  lsmdisjr  19663  gexex  19832  gsumxp2  19959  dprd0  20012  oppr1  20308  opprunit  20335  zringndrg  21427  gsummoncoe1  22244  mat0dimcrng  22406  iinopn  22838  elcls  23009  ordthaus  23320  hauscmplem  23342  regr1lem2  23676  metdseq0  24792  minveclem1  25374  minveclem3b  25378  volun  25496  dyaddisj  25547  vieta1  26270  logeftb  26542  birthdaylem1  26911  dmgmaddn0  26983  gausslemma2d  27335  lgseisenlem1  27336  2lgslem4  27367  rpvmasum  27487  sltsolem1  27637  noinfbnd2lem1  27692  madeval2  27809  made0  27829  axsegconlem6  28847  edg0iedg0  28980  numedglnl  29069  ushgredgedg  29154  ushgredgedgloop  29156  uhgr0v0e  29163  usgr1v0edg  29182  usgrexmpllem  29185  usgr1v0e  29251  nbuhgr2vtx1edgblem  29276  uvtx01vtx  29322  prcliscplgr  29339  cusgr0v  29353  vtxdg0e  29400  1loopgrvd2  29429  finsumvtxdg2ssteplem4  29474  finsumvtxdg2size  29476  isrgr  29485  fusgrregdegfi  29495  wspn0  29852  2wlkdlem8  29861  3wlkdlem8  30094  uhgr3cyclexlem  30108  1to2vfriswmgr  30206  1to3vfriswmgr  30207  frgrregorufr0  30251  frgrreg  30321  frgrregord013  30322  ex-ceil  30375  nmlno0lem  30720  minvecolem1  30801  hvsubeq0i  30990  hvsubaddi  30993  pjoc2i  31365  pjoml3i  31513  cmbr3i  31527  pjss2i  31607  hosubeq0i  31753  dmadjrnb  31833  nmlnop0iALT  31922  nmopcoadj0i  32030  stm1ri  32171  jplem2  32196  atoml2i  32310  chirredlem1  32317  cdj3lem3  32365  difininv  32444  disjnf  32497  disjpreima  32511  disjunsn  32521  f1od2  32644  wrdt2ind  32875  isunit2  33181  isdrng4  33235  lsmsnorb2  33353  ssdifidlprm  33419  fldext2chn  33708  zrhchr  33951  ddemeas  34213  braew  34219  aean  34221  eulerpartlemgh  34356  ballotlemfp1  34470  repr0  34589  hgt750lem2  34630  bnj1143  34767  nummin  35068  acycgr0v  35116  prclisacycgr  35119  cvmsss2  35242  cvmlift2lem13  35283  elrn3  35725  rankeq1o  36135  hfun  36142  bj-disj2r  36992  bj-sscon  36993  bj-0int  37065  bj-imdirco  37154  bj-pinftynminfty  37191  finxpreclem4  37358  nlpineqsn  37372  curunc  37572  tan2h  37582  poimirlem13  37603  poimirlem14  37604  poimirlem21  37611  poimirlem22  37612  asindmre  37673  totbndbnd  37759  rngosn3  37894  scott0f  38139  n0el2  38297  dfrel5  38310  dfrel6  38311  redundeq1  38593  dmqscoelseq  38625  dfeldisj5  38685  atbase  39253  llnbase  39474  lplnbase  39499  lvolbase  39543  lhpbase  39963  cdlemg31b0N  40659  cdlemg31b0a  40660  cdlemh  40782  sticksstones16  42121  sticksstones21  42126  unitscyglem3  42156  metakunt24  42187  onsupmaxb  43210  iunrelexp0  43673  frege120  43954  clsk1indlem4  44015  gneispace  44105  scotteld  44218  undisjrab  44278  zfregs2VD  44813  dvnprod  45926  fnresfnco  47018  aiotavb  47067  afvpcfv0  47123  aovpcov0  47167  aov0ov0  47170  aovov0bi  47173  fnotaovb  47175  funressndmafv2rn  47200  fmtnoprmfac1lem  47526  lighneallem2  47568  stgrvtx0  47922  isubgr3stgrlem6  47931  snlindsntor  48395  rrx2pnedifcoorneorr  48645  itschlc0xyqsol1  48694  2itscp  48709  resinsn  48795  resinsnALT  48796  opndisj  48825  istermc  49308  lanrcl  49444  ranrcl  49445