Theorem eqeq1i 2744

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

Syntax hints:   ↔ wb 207   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  eqeq12i  2757  eqabb  2878  neeq1i  2998  dfss2  3901  ssequn2  4118  ineqcom  4139  dfss7  4179  dfss4  4197  rabeq0w  4315  rabeq0  4316  disj  4378  undisj1  4390  undisj2  4391  undif  4410  undifr  4411  rabeqsn  4599  reusn  4659  rabsneu  4661  eusn  4662  tppreqb  4738  elpreqpr  4798  uniintsn  4915  iin0  5291  dfepfr  5602  epfrc  5603  dmopab3  5861  dm0rn0  5866  dm0rn0OLD  5867  rnopab3  5898  ssdmres  5965  iresn0n0  6006  imadisj  6032  args  6044  dffr3  6051  intirr  6068  dminxp  6131  dfrel3  6149  coeq0  6207  snres0  6249  sspred  6261  dffr4  6271  frpomin2  6292  frpoind  6293  cbviotavw  6449  fntpg  6545  fncnv  6558  mptfnf  6620  sbcfng  6652  f0rn0  6712  dff1o4  6775  dffv4  6824  tz6.12c  6849  fvun2  6919  fnreseql  6989  funopdmsn  7093  riota1  7334  riota2df  7336  riotaeqimp  7339  fnbrovb  7407  ovid  7497  ov  7500  ovg  7521  ovima0  7535  opiota  8001  frrlem13  8238  tz7.49c  8375  sucprcreg  9511  sucprcregOLD  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  21443  gsummoncoe1  22294  mat0dimcrng  22453  iinopn  22885  elcls  23056  ordthaus  23367  hauscmplem  23389  regr1lem2  23723  metdseq0  24838  minveclem1  25409  minveclem3b  25413  volun  25530  dyaddisj  25581  vieta1  26296  logeftb  26565  birthdaylem1  26933  dmgmaddn0  27004  gausslemma2d  27355  lgseisenlem1  27356  2lgslem4  27387  rpvmasum  27507  ltssolem1  27657  noinfbnd2lem1  27712  madeval2  27843  made0  27873  axsegconlem6  29009  edg0iedg0  29142  numedglnl  29231  ushgredgedg  29316  ushgredgedgloop  29318  uhgr0v0e  29325  usgr1v0edg  29344  usgrexmpllem  29347  usgr1v0e  29413  nbuhgr2vtx1edgblem  29438  uvtx01vtx  29484  prcliscplgr  29501  cusgr0v  29515  vtxdg0e  29561  1loopgrvd2  29590  finsumvtxdg2ssteplem4  29635  finsumvtxdg2size  29637  isrgr  29646  fusgrregdegfi  29656  wspn0  30010  2wlkdlem8  30019  3wlkdlem8  30255  uhgr3cyclexlem  30269  1to2vfriswmgr  30367  1to3vfriswmgr  30368  frgrregorufr0  30412  frgrreg  30482  frgrregord013  30483  ex-ceil  30536  nmlno0lem  30882  minvecolem1  30963  hvsubeq0i  31152  hvsubaddi  31155  pjoc2i  31527  pjoml3i  31675  cmbr3i  31689  pjss2i  31769  hosubeq0i  31915  dmadjrnb  31995  nmlnop0iALT  32084  nmopcoadj0i  32192  stm1ri  32333  jplem2  32358  atoml2i  32472  chirredlem1  32479  cdj3lem3  32527  difininv  32605  disjnf  32659  disjpreima  32673  disjunsn  32683  f1od2  32811  wrdt2ind  33032  isunit2  33321  isdrng4  33379  lsmsnorb2  33475  ssdifidlprm  33541  fldext2chn  33912  zrhchr  34158  ddemeas  34420  braew  34426  aean  34428  eulerpartlemgh  34562  ballotlemfp1  34676  repr0  34795  hgt750lem2  34836  bnj1143  34972  nummin  35274  acycgr0v  35376  prclisacycgr  35379  cvmsss2  35502  cvmlift2lem13  35543  elrn3  35990  rankeq1o  36399  hfun  36406  bj-disj2r  37381  bj-sscon  37382  bj-0int  37459  bj-imdirco  37550  bj-pinftynminfty  37587  finxpreclem4  37756  nlpineqsn  37770  curunc  37969  tan2h  37979  poimirlem13  38000  poimirlem14  38001  poimirlem21  38008  poimirlem22  38009  asindmre  38070  totbndbnd  38156  rngosn3  38291  scott0f  38536  n0el2  38702  dfrel5  38713  dfrel6  38714  redundeq1  39080  dmqscoelseq  39113  dfeldisj5  39180  atbase  39781  llnbase  40001  lplnbase  40026  lvolbase  40070  lhpbase  40490  cdlemg31b0N  41186  cdlemg31b0a  41187  cdlemh  41309  sticksstones16  42647  sticksstones21  42652  unitscyglem3  42682  onsupmaxb  43684  iunrelexp0  44146  frege120  44427  clsk1indlem4  44488  gneispace  44578  scotteld  44690  undisjrab  44750  zfregs2VD  45284  dvnprod  46392  fnresfnco  47504  aiotavb  47553  afvpcfv0  47609  aovpcov0  47653  aov0ov0  47656  aovov0bi  47659  fnotaovb  47661  funressndmafv2rn  47686  fmtnoprmfac1lem  48042  lighneallem2  48084  stgrvtx0  48453  isubgr3stgrlem6  48462  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  snlindsntor  48962  rrx2pnedifcoorneorr  49208  itschlc0xyqsol1  49257  2itscp  49272  resinsn  49362  resinsnALT  49363  opndisj  49393  istermc  49964  lanrcl  50111  ranrcl  50112