Theorem eqeq1i 2742

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

Syntax hints:   ↔ wb 206   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeq12i  2755  eqabb  2876  neeq1i  2997  dfss2  3908  ssequn2  4130  ineqcom  4151  dfss7  4192  dfss4  4210  rabeq0w  4328  rabeq0  4329  disj  4391  undisj1  4403  undisj2  4404  undif  4423  undifr  4424  rabeqsn  4612  reusn  4672  rabsneu  4674  eusn  4675  tppreqb  4749  elpreqpr  4811  uniintsn  4928  iin0  5299  dfepfr  5608  epfrc  5609  dmopab3  5868  dm0rn0  5873  dm0rn0OLD  5874  rnopab3  5905  ssdmres  5972  iresn0n0  6013  imadisj  6039  args  6051  dffr3  6058  intirr  6075  dminxp  6138  dfrel3  6156  coeq0  6214  snres0  6256  sspred  6268  dffr4  6278  frpomin2  6299  frpoind  6300  cbviotavw  6456  fntpg  6552  fncnv  6565  mptfnf  6627  sbcfng  6659  f0rn0  6719  dff1o4  6782  dffv4  6831  tz6.12c  6856  fvun2  6926  fnreseql  6994  funopdmsn  7097  riota1  7338  riota2df  7340  riotaeqimp  7343  fnbrovb  7411  ovid  7501  ov  7504  ovg  7525  ovima0  7539  opiota  8005  frrlem13  8241  tz7.49c  8378  sucprcreg  9512  zfregfr  9516  inf3lem2  9541  zfregs2  9645  frind  9665  rankxpsuc  9797  scott0s  9803  cplem1  9804  cfslb2n  10181  fin23lem26  10238  dfacfin7  10312  axdc3lem4  10366  zorn2lem7  10415  alephom  10499  fpwwe2  10557  recmulnq  10878  recexsr  11021  map2psrpr  11024  renegcli  11446  addeq0  11564  elznn0  12530  xrsupss  13252  xrinfmss  13253  prinfzo0  13644  seqf1olem1  13994  seqf1olem2  13995  sqeqori  14167  hashrabsn1  14327  hashprb  14350  hashprdifel  14351  hashbclem  14405  hash2pwpr  14429  f1oun2prg  14870  modfsummods  15747  cshwrepswhash1  17064  ismgmid  18624  smndex2dnrinv  18877  oppgid  19322  lsmdisjr  19650  gexex  19819  gsumxp2  19946  dprd0  19999  oppr1  20321  opprunit  20348  zringndrg  21458  gsummoncoe1  22283  mat0dimcrng  22445  iinopn  22877  elcls  23048  ordthaus  23359  hauscmplem  23381  regr1lem2  23715  metdseq0  24830  minveclem1  25401  minveclem3b  25405  volun  25522  dyaddisj  25573  vieta1  26289  logeftb  26560  birthdaylem1  26928  dmgmaddn0  27000  gausslemma2d  27351  lgseisenlem1  27352  2lgslem4  27383  rpvmasum  27503  ltssolem1  27653  noinfbnd2lem1  27708  madeval2  27839  made0  27869  axsegconlem6  29005  edg0iedg0  29138  numedglnl  29227  ushgredgedg  29312  ushgredgedgloop  29314  uhgr0v0e  29321  usgr1v0edg  29340  usgrexmpllem  29343  usgr1v0e  29409  nbuhgr2vtx1edgblem  29434  uvtx01vtx  29480  prcliscplgr  29497  cusgr0v  29511  vtxdg0e  29558  1loopgrvd2  29587  finsumvtxdg2ssteplem4  29632  finsumvtxdg2size  29634  isrgr  29643  fusgrregdegfi  29653  wspn0  30007  2wlkdlem8  30016  3wlkdlem8  30252  uhgr3cyclexlem  30266  1to2vfriswmgr  30364  1to3vfriswmgr  30365  frgrregorufr0  30409  frgrreg  30479  frgrregord013  30480  ex-ceil  30533  nmlno0lem  30879  minvecolem1  30960  hvsubeq0i  31149  hvsubaddi  31152  pjoc2i  31524  pjoml3i  31672  cmbr3i  31686  pjss2i  31766  hosubeq0i  31912  dmadjrnb  31992  nmlnop0iALT  32081  nmopcoadj0i  32189  stm1ri  32330  jplem2  32355  atoml2i  32469  chirredlem1  32476  cdj3lem3  32524  difininv  32602  disjnf  32655  disjpreima  32669  disjunsn  32679  f1od2  32807  wrdt2ind  33028  isunit2  33316  isdrng4  33371  lsmsnorb2  33467  ssdifidlprm  33533  fldext2chn  33888  zrhchr  34134  ddemeas  34396  braew  34402  aean  34404  eulerpartlemgh  34538  ballotlemfp1  34652  repr0  34771  hgt750lem2  34812  bnj1143  34948  nummin  35252  acycgr0v  35346  prclisacycgr  35349  cvmsss2  35472  cvmlift2lem13  35513  elrn3  35960  rankeq1o  36369  hfun  36376  bj-disj2r  37351  bj-sscon  37352  bj-0int  37429  bj-imdirco  37520  bj-pinftynminfty  37557  finxpreclem4  37724  nlpineqsn  37738  curunc  37937  tan2h  37947  poimirlem13  37968  poimirlem14  37969  poimirlem21  37976  poimirlem22  37977  asindmre  38038  totbndbnd  38124  rngosn3  38259  scott0f  38504  n0el2  38670  dfrel5  38681  dfrel6  38682  redundeq1  39048  dmqscoelseq  39081  dfeldisj5  39148  atbase  39749  llnbase  39969  lplnbase  39994  lvolbase  40038  lhpbase  40458  cdlemg31b0N  41154  cdlemg31b0a  41155  cdlemh  41277  sticksstones16  42615  sticksstones21  42620  unitscyglem3  42650  onsupmaxb  43685  iunrelexp0  44147  frege120  44428  clsk1indlem4  44489  gneispace  44579  scotteld  44691  undisjrab  44751  zfregs2VD  45285  dvnprod  46395  fnresfnco  47501  aiotavb  47550  afvpcfv0  47606  aovpcov0  47650  aov0ov0  47653  aovov0bi  47656  fnotaovb  47658  funressndmafv2rn  47683  fmtnoprmfac1lem  48039  lighneallem2  48081  stgrvtx0  48450  isubgr3stgrlem6  48459  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  snlindsntor  48959  rrx2pnedifcoorneorr  49205  itschlc0xyqsol1  49254  2itscp  49269  resinsn  49359  resinsnALT  49360  opndisj  49390  istermc  49961  lanrcl  50108  ranrcl  50109