Theorem eqeq1i 2766

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

Syntax hints:   ↔ wb 208   = wceq 1559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753

This theorem is referenced by:  eqeq12i  2779  eqabb  2900  neeq1i  3020  dfss2  3920  ssequn2  4139  ineqcom  4160  dfss7  4201  dfss4  4219  rabeq0w  4338  rabeq0  4339  disj  4401  undisj1  4413  undisj2  4414  undif  4433  undifr  4434  rabeqsn  4623  reusn  4683  rabsneu  4685  eusn  4686  tppreqb  4762  elpreqpr  4822  uniintsn  4940  iin0  5316  dfepfr  5627  epfrc  5628  dmopab3  5891  dm0rn0  5896  dm0rn0OLD  5897  rnopab3  5928  ssdmres  5995  iresn0n0  6039  imadisj  6065  args  6077  dffr3  6084  intirr  6101  dminxp  6161  dfrel3  6180  coeq0  6238  snres0  6280  sspred  6292  dffr4  6302  frpomin2  6323  frpoind  6324  cbviotavw  6480  fntpg  6576  fncnv  6589  mptfnf  6651  sbcfng  6683  f0rn0  6744  dff1o4  6810  dffv4  6859  tz6.12c  6884  fvun2  6954  fnreseql  7024  funopdmsn  7128  riota1  7369  riota2df  7371  riotaeqimp  7374  fnbrovb  7442  ovid  7532  ov  7535  ovg  7556  ovima0  7570  opiota  8035  frrlem13  8273  tz7.49c  8411  sucprcreg  9548  sucprcregOLD  9549  zfregfr  9553  inf3lem2  9578  zfregs2  9682  frind  9702  rankxpsuc  9834  scott0s  9840  cplem1  9841  cfslb2n  10219  fin23lem26  10276  dfacfin7  10350  axdc3lem4  10404  zorn2lem7  10453  alephom  10537  fpwwe2  10595  recmulnq  10916  recexsr  11059  map2psrpr  11062  renegcli  11486  addeq0  11604  elznn0  12577  xrsupss  13306  xrinfmss  13307  prinfzo0  13698  seqf1olem1  14048  seqf1olem2  14049  sqeqori  14221  hashrabsn1  14381  hashprb  14404  hashprdifel  14405  hashbclem  14459  hash2pwpr  14483  f1oun2prg  14924  modfsummods  15812  cshwrepswhash1  17129  ismgmid  18690  smndex2dnrinv  18943  oppgid  19387  lsmdisjr  19715  gexex  19884  gsumxp2  20011  dprd0  20064  oppr1  20386  opprunit  20413  zringndrg  21508  gsummoncoe1  22359  mat0dimcrng  22518  iinopn  22950  elcls  23121  ordthaus  23432  hauscmplem  23454  regr1lem2  23788  metdseq0  24903  minveclem1  25474  minveclem3b  25478  volun  25595  dyaddisj  25646  vieta1  26364  logeftb  26636  birthdaylem1  27004  dmgmaddn0  27075  gausslemma2d  27426  lgseisenlem1  27427  2lgslem4  27458  rpvmasum  27578  ltssolem1  27727  noinfbnd2lem1  27782  madeval2  27914  made0  27944  axsegconlem6  29080  edg0iedg0  29213  numedglnl  29302  ushgredgedg  29387  ushgredgedgloop  29389  uhgr0v0e  29396  usgr1v0edg  29415  usgrexmpllem  29418  usgr1v0e  29484  nbuhgr2vtx1edgblem  29509  uvtx01vtx  29555  prcliscplgr  29572  cusgr0v  29586  vtxdg0e  29632  1loopgrvd2  29661  finsumvtxdg2ssteplem4  29706  finsumvtxdg2size  29708  isrgr  29717  fusgrregdegfi  29727  wspn0  30081  2wlkdlem8  30090  3wlkdlem8  30326  uhgr3cyclexlem  30340  1to2vfriswmgr  30438  1to3vfriswmgr  30439  frgrregorufr0  30483  frgrreg  30553  frgrregord013  30554  ex-ceil  30607  nmlno0lem  30953  minvecolem1  31034  hvsubeq0i  31223  hvsubaddi  31226  pjoc2i  31598  pjoml3i  31746  cmbr3i  31760  pjss2i  31840  hosubeq0i  31986  dmadjrnb  32066  nmlnop0iALT  32155  nmopcoadj0i  32263  stm1ri  32404  jplem2  32429  atoml2i  32543  chirredlem1  32550  cdj3lem3  32598  difininv  32676  disjnf  32730  disjpreima  32744  disjunsn  32754  f1od2  32882  wrdt2ind  33092  isunit2  33381  isdrng4  33443  lsmsnorb2  33539  ssdifidlprm  33606  fldext2chn  33986  zrhchr  34232  ddemeas  34494  braew  34500  aean  34502  eulerpartlemgh  34636  ballotlemfp1  34750  repr0  34866  hgt750lem2  34907  bnj1143  35046  nummin  35350  acycgr0v  35459  prclisacycgr  35462  cvmsss2  35585  cvmlift2lem13  35626  elrn3  36073  rankeq1o  36482  hfun  36489  bj-disj2r  37474  bj-sscon  37475  bj-0int  37552  bj-imdirco  37643  bj-pinftynminfty  37680  finxpreclem4  37849  nlpineqsn  37863  curunc  38062  tan2h  38072  poimirlem13  38093  poimirlem14  38094  poimirlem21  38101  poimirlem22  38102  asindmre  38163  totbndbnd  38249  rngosn3  38384  scott0f  38629  n0el2  38795  dfrel5  38806  dfrel6  38807  redundeq1  39173  dmqscoelseq  39206  dfeldisj5  39273  atbase  39874  llnbase  40094  lplnbase  40119  lvolbase  40163  lhpbase  40583  cdlemg31b0N  41279  cdlemg31b0a  41280  cdlemh  41402  sticksstones16  42740  sticksstones21  42745  unitscyglem3  42775  onsupmaxb  43777  iunrelexp0  44239  frege120  44520  clsk1indlem4  44581  gneispace  44671  scotteld  44783  undisjrab  44843  zfregs2VD  45377  dvnprod  46484  fnresfnco  47596  aiotavb  47645  afvpcfv0  47701  aovpcov0  47745  aov0ov0  47748  aovov0bi  47751  fnotaovb  47753  funressndmafv2rn  47778  fmtnoprmfac1lem  48134  lighneallem2  48176  stgrvtx0  48545  isubgr3stgrlem6  48554  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  snlindsntor  49054  rrx2pnedifcoorneorr  49300  itschlc0xyqsol1  49349  2itscp  49364  resinsn  49454  resinsnALT  49455  opndisj  49485  istermc  50056  lanrcl  50203  ranrcl  50204