Theorem eqeq1i 2741

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

Syntax hints:   ↔ wb 206   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  eqeq12i  2754  eqabb  2875  neeq1i  2996  dfss2  3919  ssequn2  4141  ineqcom  4162  sseqin2  4175  dfss7  4203  dfss4  4221  rabeq0w  4339  rabeq0  4340  disj  4402  disjr  4403  undisj1  4414  undisj2  4415  undif  4434  undifr  4435  undifrOLD  4436  uneqdifeq  4445  rabeqsn  4624  reusn  4684  rabsneu  4686  eusn  4687  tppreqb  4761  elpreqpr  4823  uniintsn  4940  iin0  5307  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  6993  funopdmsn  7095  riota1  7336  riota2df  7338  riotaeqimp  7341  fnbrovb  7409  ovid  7499  ov  7502  ovg  7523  ovima0  7537  opiota  8003  frrlem13  8240  tz7.49c  8377  sucprcreg  9509  zfregfr  9513  inf3lem2  9538  zfregs2  9642  frind  9662  rankxpsuc  9794  scott0s  9800  cplem1  9801  cfslb2n  10178  fin23lem26  10235  dfacfin7  10309  axdc3lem4  10363  zorn2lem7  10412  alephom  10496  fpwwe2  10554  recmulnq  10875  recexsr  11018  map2psrpr  11021  renegcli  11442  addeq0  11560  elznn0  12503  xrsupss  13224  xrinfmss  13225  prinfzo0  13614  seqf1olem1  13964  seqf1olem2  13965  sqeqori  14137  hashrabsn1  14297  hashprb  14320  hashprdifel  14321  hashbclem  14375  hash2pwpr  14399  f1oun2prg  14840  modfsummods  15716  cshwrepswhash1  17030  ismgmid  18590  smndex2dnrinv  18840  oppgid  19285  lsmdisjr  19613  gexex  19782  gsumxp2  19909  dprd0  19962  oppr1  20286  opprunit  20313  zringndrg  21423  gsummoncoe1  22252  mat0dimcrng  22414  iinopn  22846  elcls  23017  ordthaus  23328  hauscmplem  23350  regr1lem2  23684  metdseq0  24799  minveclem1  25380  minveclem3b  25384  volun  25502  dyaddisj  25553  vieta1  26276  logeftb  26548  birthdaylem1  26917  dmgmaddn0  26989  gausslemma2d  27341  lgseisenlem1  27342  2lgslem4  27373  rpvmasum  27493  ltssolem1  27643  noinfbnd2lem1  27698  madeval2  27829  made0  27859  axsegconlem6  28995  edg0iedg0  29128  numedglnl  29217  ushgredgedg  29302  ushgredgedgloop  29304  uhgr0v0e  29311  usgr1v0edg  29330  usgrexmpllem  29333  usgr1v0e  29399  nbuhgr2vtx1edgblem  29424  uvtx01vtx  29470  prcliscplgr  29487  cusgr0v  29501  vtxdg0e  29548  1loopgrvd2  29577  finsumvtxdg2ssteplem4  29622  finsumvtxdg2size  29624  isrgr  29633  fusgrregdegfi  29643  wspn0  29997  2wlkdlem8  30006  3wlkdlem8  30242  uhgr3cyclexlem  30256  1to2vfriswmgr  30354  1to3vfriswmgr  30355  frgrregorufr0  30399  frgrreg  30469  frgrregord013  30470  ex-ceil  30523  nmlno0lem  30868  minvecolem1  30949  hvsubeq0i  31138  hvsubaddi  31141  pjoc2i  31513  pjoml3i  31661  cmbr3i  31675  pjss2i  31755  hosubeq0i  31901  dmadjrnb  31981  nmlnop0iALT  32070  nmopcoadj0i  32178  stm1ri  32319  jplem2  32344  atoml2i  32458  chirredlem1  32465  cdj3lem3  32513  difininv  32592  disjnf  32645  disjpreima  32659  disjunsn  32669  f1od2  32798  wrdt2ind  33035  isunit2  33322  isdrng4  33377  lsmsnorb2  33473  ssdifidlprm  33539  fldext2chn  33885  zrhchr  34131  ddemeas  34393  braew  34399  aean  34401  eulerpartlemgh  34535  ballotlemfp1  34649  repr0  34768  hgt750lem2  34809  bnj1143  34946  nummin  35249  acycgr0v  35342  prclisacycgr  35345  cvmsss2  35468  cvmlift2lem13  35509  elrn3  35956  rankeq1o  36365  hfun  36372  bj-disj2r  37229  bj-sscon  37230  bj-0int  37306  bj-imdirco  37395  bj-pinftynminfty  37432  finxpreclem4  37599  nlpineqsn  37613  curunc  37803  tan2h  37813  poimirlem13  37834  poimirlem14  37835  poimirlem21  37842  poimirlem22  37843  asindmre  37904  totbndbnd  37990  rngosn3  38125  scott0f  38370  n0el2  38528  dfrel5  38539  dfrel6  38540  redundeq1  38886  dmqscoelseq  38920  dfeldisj5  38980  atbase  39549  llnbase  39769  lplnbase  39794  lvolbase  39838  lhpbase  40258  cdlemg31b0N  40954  cdlemg31b0a  40955  cdlemh  41077  sticksstones16  42416  sticksstones21  42421  unitscyglem3  42451  onsupmaxb  43481  iunrelexp0  43943  frege120  44224  clsk1indlem4  44285  gneispace  44375  scotteld  44487  undisjrab  44547  zfregs2VD  45081  dvnprod  46193  fnresfnco  47287  aiotavb  47336  afvpcfv0  47392  aovpcov0  47436  aov0ov0  47439  aovov0bi  47442  fnotaovb  47444  funressndmafv2rn  47469  fmtnoprmfac1lem  47810  lighneallem2  47852  stgrvtx0  48208  isubgr3stgrlem6  48217  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  snlindsntor  48717  rrx2pnedifcoorneorr  48963  itschlc0xyqsol1  49012  2itscp  49027  resinsn  49117  resinsnALT  49118  opndisj  49148  istermc  49719  lanrcl  49866  ranrcl  49867