Theorem eqeq1i 2738

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 2737	. 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 2705

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

This theorem is referenced by:  eqeq12i  2751  eqabb  2872  neeq1i  2993  dfss2  3916  ssequn2  4138  ineqcom  4159  sseqin2  4172  dfss7  4200  dfss4  4218  rabeq0w  4336  rabeq0  4337  disj  4399  disjr  4400  undisj1  4411  undisj2  4412  undif  4431  undifr  4432  undifrOLD  4433  uneqdifeq  4442  rabeqsn  4621  reusn  4681  rabsneu  4683  eusn  4684  tppreqb  4758  elpreqpr  4820  uniintsn  4937  iin0  5304  dfepfr  5605  epfrc  5606  dmopab3  5865  dm0rn0  5870  dm0rn0OLD  5871  rnopab3  5902  ssdmres  5969  iresn0n0  6010  imadisj  6036  args  6048  dffr3  6055  intirr  6072  dminxp  6135  dfrel3  6153  coeq0  6211  snres0  6253  sspred  6265  dffr4  6275  frpomin2  6296  frpoind  6297  cbviotavw  6453  fntpg  6549  fncnv  6562  mptfnf  6624  sbcfng  6656  f0rn0  6716  dff1o4  6779  dffv4  6828  tz6.12c  6853  fvun2  6923  fnreseql  6990  funopdmsn  7092  riota1  7333  riota2df  7335  riotaeqimp  7338  fnbrovb  7406  ovid  7496  ov  7499  ovg  7520  ovima0  7534  opiota  8000  frrlem13  8237  tz7.49c  8374  sucprcreg  9501  zfregfr  9505  inf3lem2  9530  zfregs2  9634  frind  9654  rankxpsuc  9786  scott0s  9792  cplem1  9793  cfslb2n  10170  fin23lem26  10227  dfacfin7  10301  axdc3lem4  10355  zorn2lem7  10404  alephom  10487  fpwwe2  10545  recmulnq  10866  recexsr  11009  map2psrpr  11012  renegcli  11433  addeq0  11551  elznn0  12494  xrsupss  13215  xrinfmss  13216  prinfzo0  13605  seqf1olem1  13955  seqf1olem2  13956  sqeqori  14128  hashrabsn1  14288  hashprb  14311  hashprdifel  14312  hashbclem  14366  hash2pwpr  14390  f1oun2prg  14831  modfsummods  15707  cshwrepswhash1  17021  ismgmid  18581  smndex2dnrinv  18831  oppgid  19276  lsmdisjr  19604  gexex  19773  gsumxp2  19900  dprd0  19953  oppr1  20277  opprunit  20304  zringndrg  21414  gsummoncoe1  22243  mat0dimcrng  22405  iinopn  22837  elcls  23008  ordthaus  23319  hauscmplem  23341  regr1lem2  23675  metdseq0  24790  minveclem1  25371  minveclem3b  25375  volun  25493  dyaddisj  25544  vieta1  26267  logeftb  26539  birthdaylem1  26908  dmgmaddn0  26980  gausslemma2d  27332  lgseisenlem1  27333  2lgslem4  27364  rpvmasum  27484  sltsolem1  27634  noinfbnd2lem1  27689  madeval2  27814  made0  27838  axsegconlem6  28921  edg0iedg0  29054  numedglnl  29143  ushgredgedg  29228  ushgredgedgloop  29230  uhgr0v0e  29237  usgr1v0edg  29256  usgrexmpllem  29259  usgr1v0e  29325  nbuhgr2vtx1edgblem  29350  uvtx01vtx  29396  prcliscplgr  29413  cusgr0v  29427  vtxdg0e  29474  1loopgrvd2  29503  finsumvtxdg2ssteplem4  29548  finsumvtxdg2size  29550  isrgr  29559  fusgrregdegfi  29569  wspn0  29923  2wlkdlem8  29932  3wlkdlem8  30168  uhgr3cyclexlem  30182  1to2vfriswmgr  30280  1to3vfriswmgr  30281  frgrregorufr0  30325  frgrreg  30395  frgrregord013  30396  ex-ceil  30449  nmlno0lem  30794  minvecolem1  30875  hvsubeq0i  31064  hvsubaddi  31067  pjoc2i  31439  pjoml3i  31587  cmbr3i  31601  pjss2i  31681  hosubeq0i  31827  dmadjrnb  31907  nmlnop0iALT  31996  nmopcoadj0i  32104  stm1ri  32245  jplem2  32270  atoml2i  32384  chirredlem1  32391  cdj3lem3  32439  difininv  32518  disjnf  32571  disjpreima  32585  disjunsn  32595  f1od2  32726  wrdt2ind  32963  isunit2  33250  isdrng4  33305  lsmsnorb2  33401  ssdifidlprm  33467  fldext2chn  33813  zrhchr  34059  ddemeas  34321  braew  34327  aean  34329  eulerpartlemgh  34463  ballotlemfp1  34577  repr0  34696  hgt750lem2  34737  bnj1143  34874  nummin  35176  acycgr0v  35264  prclisacycgr  35267  cvmsss2  35390  cvmlift2lem13  35431  elrn3  35878  rankeq1o  36287  hfun  36294  bj-disj2r  37145  bj-sscon  37146  bj-0int  37218  bj-imdirco  37307  bj-pinftynminfty  37344  finxpreclem4  37511  nlpineqsn  37525  curunc  37715  tan2h  37725  poimirlem13  37746  poimirlem14  37747  poimirlem21  37754  poimirlem22  37755  asindmre  37816  totbndbnd  37902  rngosn3  38037  scott0f  38282  n0el2  38440  dfrel5  38451  dfrel6  38452  redundeq1  38798  dmqscoelseq  38832  dfeldisj5  38892  atbase  39461  llnbase  39681  lplnbase  39706  lvolbase  39750  lhpbase  40170  cdlemg31b0N  40866  cdlemg31b0a  40867  cdlemh  40989  sticksstones16  42328  sticksstones21  42333  unitscyglem3  42363  onsupmaxb  43396  iunrelexp0  43859  frege120  44140  clsk1indlem4  44201  gneispace  44291  scotteld  44403  undisjrab  44463  zfregs2VD  44997  dvnprod  46109  fnresfnco  47203  aiotavb  47252  afvpcfv0  47308  aovpcov0  47352  aov0ov0  47355  aovov0bi  47358  fnotaovb  47360  funressndmafv2rn  47385  fmtnoprmfac1lem  47726  lighneallem2  47768  stgrvtx0  48124  isubgr3stgrlem6  48133  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  pgnbgreunbgrlem2lem3  48278  snlindsntor  48633  rrx2pnedifcoorneorr  48879  itschlc0xyqsol1  48928  2itscp  48943  resinsn  49033  resinsnALT  49034  opndisj  49064  istermc  49635  lanrcl  49782  ranrcl  49783