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 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

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

This theorem is referenced by:  eqeq12i  2752  eqabb  2878  neeq1i  3002  dfss2  3980  ssequn2  4198  ineqcom  4217  sseqin2  4230  dfss7  4256  dfss4  4274  rabeq0w  4392  rabeq0  4393  disj  4455  disjr  4456  undisj1  4467  undisj2  4468  undif  4487  undifr  4488  undifrOLD  4489  uneqdifeq  4498  rabeqsn  4671  reusn  4731  rabsneu  4733  eusn  4734  tppreqb  4809  elpreqpr  4871  uniintsn  4989  iin0  5367  dfepfr  5672  epfrc  5673  dmopab3  5932  dm0rn0  5937  rnopab3  5969  ssdmres  6032  iresn0n0  6073  imadisj  6099  args  6112  dffr3  6119  intirr  6140  dminxp  6201  dfrel3  6219  coeq0  6276  snres0  6319  sspred  6331  dffr4  6342  frpomin2  6363  frpoind  6364  tz6.26OLD  6370  wfiOLD  6373  cbviotavw  6523  fntpg  6627  fncnv  6640  mptfnf  6703  sbcfng  6733  f0rn0  6793  dff1o4  6856  dffv4  6903  tz6.12c  6928  fvun2  7000  fnreseql  7067  funopdmsn  7169  riota1  7408  riota2df  7410  riotaeqimp  7413  fnbrovb  7481  ovid  7573  ov  7576  ovg  7597  ovima0  7611  opiota  8082  frrlem13  8321  wfrlem8OLD  8354  tz7.49c  8484  sucprcreg  9638  zfregfr  9642  inf3lem2  9666  zfregs2  9770  frind  9787  rankxpsuc  9919  scott0s  9925  cplem1  9926  cfslb2n  10305  fin23lem26  10362  dfacfin7  10436  axdc3lem4  10490  zorn2lem7  10539  alephom  10622  fpwwe2  10680  recmulnq  11001  recexsr  11144  map2psrpr  11147  renegcli  11567  addeq0  11683  elznn0  12625  xrsupss  13347  xrinfmss  13348  prinfzo0  13734  seqf1olem1  14078  seqf1olem2  14079  sqeqori  14249  hashrabsn1  14409  hashprb  14432  hashprdifel  14433  hashbclem  14487  hash2pwpr  14511  f1oun2prg  14952  modfsummods  15825  cshwrepswhash1  17136  ismgmid  18690  smndex2dnrinv  18940  oppgid  19389  lsmdisjr  19716  gexex  19885  gsumxp2  20012  dprd0  20065  oppr1  20366  opprunit  20393  zringndrg  21496  gsummoncoe1  22327  mat0dimcrng  22491  iinopn  22923  elcls  23096  ordthaus  23407  hauscmplem  23429  regr1lem2  23763  metdseq0  24889  minveclem1  25471  minveclem3b  25475  volun  25593  dyaddisj  25644  vieta1  26368  logeftb  26639  birthdaylem1  27008  dmgmaddn0  27080  gausslemma2d  27432  lgseisenlem1  27433  2lgslem4  27464  rpvmasum  27584  sltsolem1  27734  noinfbnd2lem1  27789  madeval2  27906  made0  27926  axsegconlem6  28951  edg0iedg0  29086  numedglnl  29175  ushgredgedg  29260  ushgredgedgloop  29262  uhgr0v0e  29269  usgr1v0edg  29288  usgrexmpllem  29291  usgr1v0e  29357  nbuhgr2vtx1edgblem  29382  uvtx01vtx  29428  prcliscplgr  29445  cusgr0v  29459  vtxdg0e  29506  1loopgrvd2  29535  finsumvtxdg2ssteplem4  29580  finsumvtxdg2size  29582  isrgr  29591  fusgrregdegfi  29601  wspn0  29953  2wlkdlem8  29962  3wlkdlem8  30195  uhgr3cyclexlem  30209  1to2vfriswmgr  30307  1to3vfriswmgr  30308  frgrregorufr0  30352  frgrreg  30422  frgrregord013  30423  ex-ceil  30476  nmlno0lem  30821  minvecolem1  30902  hvsubeq0i  31091  hvsubaddi  31094  pjoc2i  31466  pjoml3i  31614  cmbr3i  31628  pjss2i  31708  hosubeq0i  31854  dmadjrnb  31934  nmlnop0iALT  32023  nmopcoadj0i  32131  stm1ri  32272  jplem2  32297  atoml2i  32411  chirredlem1  32418  cdj3lem3  32466  difininv  32544  disjnf  32589  disjpreima  32603  disjunsn  32613  f1od2  32738  wrdt2ind  32922  isunit2  33229  isdrng4  33278  lsmsnorb2  33399  ssdifidlprm  33465  zrhchr  33936  ddemeas  34216  braew  34222  aean  34224  eulerpartlemgh  34359  ballotlemfp1  34472  repr0  34604  hgt750lem2  34645  bnj1143  34782  nummin  35083  acycgr0v  35132  prclisacycgr  35135  cvmsss2  35258  cvmlift2lem13  35299  elrn3  35741  rankeq1o  36152  hfun  36159  bj-disj2r  37010  bj-sscon  37011  bj-0int  37083  bj-imdirco  37172  bj-pinftynminfty  37209  finxpreclem4  37376  nlpineqsn  37390  curunc  37588  tan2h  37598  poimirlem13  37619  poimirlem14  37620  poimirlem21  37627  poimirlem22  37628  asindmre  37689  totbndbnd  37775  rngosn3  37910  scott0f  38155  n0el2  38314  dfrel5  38327  dfrel6  38328  redundeq1  38610  dmqscoelseq  38642  dfeldisj5  38702  atbase  39270  llnbase  39491  lplnbase  39516  lvolbase  39560  lhpbase  39980  cdlemg31b0N  40676  cdlemg31b0a  40677  cdlemh  40799  sticksstones16  42143  sticksstones21  42148  unitscyglem3  42178  metakunt24  42209  onsupmaxb  43227  iunrelexp0  43691  frege120  43972  clsk1indlem4  44033  gneispace  44123  scotteld  44241  undisjrab  44301  zfregs2VD  44838  dvnprod  45904  fnresfnco  46990  aiotavb  47039  afvpcfv0  47095  aovpcov0  47139  aov0ov0  47142  aovov0bi  47145  fnotaovb  47147  funressndmafv2rn  47172  fmtnoprmfac1lem  47488  lighneallem2  47530  stgrvtx0  47864  isubgr3stgrlem6  47873  snlindsntor  48316  rrx2pnedifcoorneorr  48566  itschlc0xyqsol1  48615  2itscp  48630  opndisj  48698