Theorem eqeq1i 2615

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

Syntax hints:   ↔ wb 195   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  eqeq12i  2624  neeq1i  2846  ssequn2  3748  sseqin2  3779  dfss1OLD  3780  dfss4  3820  rabeq0  3911  disj  3969  disjr  3970  undisj1  3981  undisj2  3982  undif  4001  uneqdifeq  4009  uneqdifeqOLD  4010  reusn  4206  rabsneu  4208  eusn  4209  tppreqb  4277  elpreqpr  4334  uniintsn  4449  iin0  4765  opeqsn  4892  dfepfr  5023  epfrc  5024  dmopab3  5259  dm0rn0  5263  ssdmres  5340  imadisj  5403  args  5412  dffr3  5417  intirr  5433  dminxp  5493  dfrel3  5510  coeq0  5561  sspred  5605  dffr4  5613  tz6.26  5628  wfi  5630  unisuc  5718  fntpg  5862  fncnv  5876  mptfnf  5928  sbcfng  5955  f0rn0  6003  dff1o4  6058  dffv4  6100  fvun2  6180  fnreseql  6235  riota1  6529  riota2df  6531  fnotovb  6592  ovid  6675  ov  6678  ovg  6697  ovima0  6711  opiota  7118  wfrlem8  7309  tz7.49c  7428  sucprcreg  8389  zfregfr  8392  inf3lem2  8409  zfregs2  8492  rankxpsuc  8628  scott0s  8634  cplem1  8635  cfslb2n  8973  fin23lem26  9030  dfacfin7  9104  axdc3lem4  9158  zorn2lem7  9207  alephom  9286  fpwwe2  9344  recmulnq  9665  recexsr  9807  map2psrpr  9810  renegcli  10221  elznn0  11269  xrsupss  12011  xrinfmss  12012  seqf1olem1  12702  seqf1olem2  12703  sqeqori  12838  hashrabsn1  13024  hashprb  13046  hashprdifel  13047  hashbclem  13093  hash2pwpr  13115  swrdccat3a  13345  f1oun2prg  13512  modfsummods  14366  cshwrepswhash1  15647  ismgmid  17087  oppgid  17609  lsmdisjr  17920  gexex  18079  dprd0  18253  oppr1  18457  opprunit  18484  opprdomn  19122  gsummoncoe1  19495  zringndrg  19657  mat0dimcrng  20095  iinopn  20532  elcls  20687  ordthaus  20998  hauscmplem  21019  regr1lem2  21353  metdseq0  22465  minveclem1  23003  minveclem3b  23007  volun  23120  dyaddisj  23170  vieta1  23871  logeftb  24134  birthdaylem1  24478  dmgmaddn0  24549  gausslemma2d  24899  lgseisenlem1  24900  2lgslem4  24931  rpvmasum  25015  axsegconlem6  25602  usgraedgprv  25905  wlkdvspthlem  26137  wlknwwlknsur  26240  wlkiswwlksur  26247  clwlkfclwwlk1hashn  26368  clwlkfoclwwlk  26372  1to3vfriswmgra  26534  frgrawopreg2  26578  ex-ceil  26697  nmlno0lem  27032  minvecolem1  27114  hvsubeq0i  27304  hvsubaddi  27307  pjoc2i  27681  pjoml3i  27829  cmbr3i  27843  pjss2i  27923  hosubeq0i  28069  dmadjrnb  28149  nmlnop0iALT  28238  nmopcoadj0i  28346  stm1ri  28487  jplem2  28512  atoml2i  28626  chirredlem1  28633  cdj3lem3  28681  disjnf  28766  disjpreima  28779  disjunsn  28789  f1od2  28887  addeq0  28898  zrhchr  29348  ddemeas  29626  braew  29632  aean  29634  eulerpartlemgh  29767  ballotlemfp1  29880  bnj1143  30115  cvmsss2  30510  cvmlift2lem13  30551  elrn3  30906  br1steq  30917  br2ndeq  30918  frind  30984  sltsolem1  31067  rankeq1o  31448  hfun  31455  bj-pinftynminfty  32291  finxpreclem4  32407  curunc  32561  tan2h  32571  poimirlem13  32592  poimirlem14  32593  poimirlem21  32600  poimirlem22  32601  asindmre  32665  totbndbnd  32758  rngosn3  32893  scott0f  33147  atbase  33594  llnbase  33813  lplnbase  33838  lvolbase  33882  lhpbase  34302  cdlemg31b0N  35000  cdlemg31b0a  35001  cdlemh  35123  iunrelexp0  37013  frege120  37297  clsk1indlem4  37362  gneispace  37452  undisjrab  37527  zfregs2VD  38098  dvnprod  38839  fnresfnco  39855  afvpcfv0  39875  aovpcov0  39919  aov0ov0  39922  aovov0bi  39925  fnotaovb  39927  fmtnoprmfac1lem  40014  lighneallem2  40061  riotaeqimp  40338  prinfzo0  40363  ushgredgedga  40456  ushgredgedgaloop  40458  uhgr0v0e  40464  usgrexmpllem  40484  usgr1v0e  40545  nbuhgr2vtx1edgblem  40573  uvtxa01vtx0  40623  uvtxa01vtx  40624  cusgr0v  40650  vtxdg0e  40689  1loopgrvd2  40718  isrgr  40759  fusgrregdegfi  40769  wlknwwlksnsur  41087  wlkwwlksur  41094  21wlkdlem8  41140  clwlksfclwwlk1hashn  41266  clwlksfoclwwlk  41270  31wlkdlem8  41334  uhgr3cyclexlem  41348  1to2vfriswmgr  41449  1to3vfriswmgr  41450  frgrwopreg2  41488  av-frgrareg  41548  av-frgraregord013  41549  snlindsntor  42054