Theorem eqeq1i 2826

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

Syntax hints:   ↔ wb 208   = wceq 1537

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 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  eqeq12i  2836  neeq1i  3080  ssequn2  4159  sseqin2  4192  dfss7  4217  dfss4  4235  rabeq0  4338  disj  4399  disjr  4400  undisj1  4411  undisj2  4412  undif  4430  uneqdifeq  4438  rabeqsn  4606  reusn  4663  rabsneu  4665  eusn  4666  tppreqb  4738  elpreqpr  4797  uniintsn  4913  iin0  5261  dfepfr  5540  epfrc  5541  dmopab3  5788  dm0rn0  5795  ssdmres  5876  iresn0n0  5923  imadisj  5948  args  5957  dffr3  5962  intirr  5978  dminxp  6037  dfrel3  6055  coeq0  6108  sspred  6156  dffr4  6164  tz6.26  6179  wfi  6181  unisuc  6267  fntpg  6414  fncnv  6427  mptfnf  6483  sbcfng  6511  f0rn0  6564  dff1o4  6623  dffv4  6667  fvun2  6755  fnreseql  6818  funopdmsn  6912  riota1  7135  riota2df  7137  riotaeqimp  7140  fnbrovb  7205  ovid  7291  ov  7294  ovg  7313  ovima0  7327  opiota  7757  wfrlem8  7962  tz7.49c  8082  sucprcreg  9065  zfregfr  9068  inf3lem2  9092  zfregs2  9175  rankxpsuc  9311  scott0s  9317  cplem1  9318  cfslb2n  9690  fin23lem26  9747  dfacfin7  9821  axdc3lem4  9875  zorn2lem7  9924  alephom  10007  fpwwe2  10065  recmulnq  10386  recexsr  10529  map2psrpr  10532  renegcli  10947  addeq0  11063  elznn0  11997  xrsupss  12703  xrinfmss  12704  prinfzo0  13077  seqf1olem1  13410  seqf1olem2  13411  sqeqori  13577  hashrabsn1  13736  hashprb  13759  hashprdifel  13760  hashbclem  13811  hash2pwpr  13835  f1oun2prg  14279  modfsummods  15148  cshwrepswhash1  16436  ismgmid  17875  smndex2dnrinv  18080  oppgid  18484  lsmdisjr  18810  gexex  18973  gsumxp2  19100  dprd0  19153  oppr1  19384  opprunit  19411  opprdomn  20074  gsummoncoe1  20472  zringndrg  20637  mat0dimcrng  21079  iinopn  21510  elcls  21681  ordthaus  21992  hauscmplem  22014  regr1lem2  22348  metdseq0  23462  minveclem1  24027  minveclem3b  24031  volun  24146  dyaddisj  24197  vieta1  24901  logeftb  25167  birthdaylem1  25529  dmgmaddn0  25600  gausslemma2d  25950  lgseisenlem1  25951  2lgslem4  25982  rpvmasum  26102  axsegconlem6  26708  edg0iedg0  26840  numedglnl  26929  ushgredgedg  27011  ushgredgedgloop  27013  uhgr0v0e  27020  usgr1v0edg  27039  usgrexmpllem  27042  usgr1v0e  27108  nbuhgr2vtx1edgblem  27133  uvtx01vtx  27179  prcliscplgr  27196  cusgr0v  27210  vtxdg0e  27256  1loopgrvd2  27285  finsumvtxdg2ssteplem4  27330  finsumvtxdg2size  27332  isrgr  27341  fusgrregdegfi  27351  wspn0  27703  2wlkdlem8  27712  3wlkdlem8  27946  uhgr3cyclexlem  27960  1to2vfriswmgr  28058  1to3vfriswmgr  28059  frgrregorufr0  28103  frgrreg  28173  frgrregord013  28174  ex-ceil  28227  nmlno0lem  28570  minvecolem1  28651  hvsubeq0i  28840  hvsubaddi  28843  pjoc2i  29215  pjoml3i  29363  cmbr3i  29377  pjss2i  29457  hosubeq0i  29603  dmadjrnb  29683  nmlnop0iALT  29772  nmopcoadj0i  29880  stm1ri  30021  jplem2  30046  atoml2i  30160  chirredlem1  30167  cdj3lem3  30215  difininv  30279  undifr  30284  disjnf  30320  disjpreima  30334  disjunsn  30344  f1od2  30457  wrdt2ind  30627  zrhchr  31217  ddemeas  31495  braew  31501  aean  31503  eulerpartlemgh  31636  ballotlemfp1  31749  repr0  31882  hgt750lem2  31923  bnj1143  32062  acycgr0v  32395  prclisacycgr  32398  cvmsss2  32521  cvmlift2lem13  32562  elrn3  32998  frpomin2  33079  frpoind  33080  frind  33085  frrlem13  33135  sltsolem1  33180  madeval2  33290  rankeq1o  33632  hfun  33639  bj-disj2r  34343  bj-sscon  34344  bj-0int  34396  bj-pinftynminfty  34512  finxpreclem4  34678  nlpineqsn  34692  curunc  34889  tan2h  34899  poimirlem13  34920  poimirlem14  34921  poimirlem21  34928  poimirlem22  34929  asindmre  34992  totbndbnd  35082  rngosn3  35217  scott0f  35462  ineqcom  35519  n0el2  35605  dfrel5  35618  dfrel6  35619  redundeq1  35879  dmqscoelseq  35910  dfeldisj5  35969  atbase  36440  llnbase  36660  lplnbase  36685  lvolbase  36729  lhpbase  37149  cdlemg31b0N  37845  cdlemg31b0a  37846  cdlemh  37968  iunrelexp0  40067  frege120  40349  clsk1indlem4  40414  gneispace  40504  scotteld  40602  undisjrab  40658  zfregs2VD  41195  dvnprod  42254  fnresfnco  43296  aiotavb  43310  afvpcfv0  43365  aovpcov0  43409  aov0ov0  43412  aovov0bi  43415  fnotaovb  43417  funressndmafv2rn  43442  fmtnoprmfac1lem  43746  lighneallem2  43791  snlindsntor  44546  rrx2pnedifcoorneorr  44724  itschlc0xyqsol1  44773  2itscp  44788