Theorem eqeq1i 2734

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

Syntax hints:   ↔ wb 206   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  eqeq12i  2747  eqabb  2867  neeq1i  2989  dfss2  3921  ssequn2  4140  ineqcom  4161  sseqin2  4174  dfss7  4202  dfss4  4220  rabeq0w  4338  rabeq0  4339  disj  4401  disjr  4402  undisj1  4413  undisj2  4414  undif  4433  undifr  4434  undifrOLD  4435  uneqdifeq  4444  rabeqsn  4619  reusn  4679  rabsneu  4681  eusn  4682  tppreqb  4756  elpreqpr  4818  uniintsn  4935  iin0  5301  dfepfr  5603  epfrc  5604  dmopab3  5862  dm0rn0  5867  rnopab3  5898  ssdmres  5964  iresn0n0  6005  imadisj  6031  args  6043  dffr3  6050  intirr  6067  dminxp  6129  dfrel3  6147  coeq0  6204  snres0  6246  sspred  6258  dffr4  6268  frpomin2  6289  frpoind  6290  cbviotavw  6446  fntpg  6542  fncnv  6555  mptfnf  6617  sbcfng  6649  f0rn0  6709  dff1o4  6772  dffv4  6819  tz6.12c  6844  fvun2  6915  fnreseql  6982  funopdmsn  7084  riota1  7327  riota2df  7329  riotaeqimp  7332  fnbrovb  7400  ovid  7490  ov  7493  ovg  7514  ovima0  7528  opiota  7994  frrlem13  8231  tz7.49c  8368  sucprcreg  9496  zfregfr  9500  inf3lem2  9525  zfregs2  9629  frind  9646  rankxpsuc  9778  scott0s  9784  cplem1  9785  cfslb2n  10162  fin23lem26  10219  dfacfin7  10293  axdc3lem4  10347  zorn2lem7  10396  alephom  10479  fpwwe2  10537  recmulnq  10858  recexsr  11001  map2psrpr  11004  renegcli  11425  addeq0  11543  elznn0  12486  xrsupss  13211  xrinfmss  13212  prinfzo0  13601  seqf1olem1  13948  seqf1olem2  13949  sqeqori  14121  hashrabsn1  14281  hashprb  14304  hashprdifel  14305  hashbclem  14359  hash2pwpr  14383  f1oun2prg  14824  modfsummods  15700  cshwrepswhash1  17014  ismgmid  18539  smndex2dnrinv  18789  oppgid  19235  lsmdisjr  19563  gexex  19732  gsumxp2  19859  dprd0  19912  oppr1  20235  opprunit  20262  zringndrg  21375  gsummoncoe1  22193  mat0dimcrng  22355  iinopn  22787  elcls  22958  ordthaus  23269  hauscmplem  23291  regr1lem2  23625  metdseq0  24741  minveclem1  25322  minveclem3b  25326  volun  25444  dyaddisj  25495  vieta1  26218  logeftb  26490  birthdaylem1  26859  dmgmaddn0  26931  gausslemma2d  27283  lgseisenlem1  27284  2lgslem4  27315  rpvmasum  27435  sltsolem1  27585  noinfbnd2lem1  27640  madeval2  27763  made0  27787  axsegconlem6  28867  edg0iedg0  29000  numedglnl  29089  ushgredgedg  29174  ushgredgedgloop  29176  uhgr0v0e  29183  usgr1v0edg  29202  usgrexmpllem  29205  usgr1v0e  29271  nbuhgr2vtx1edgblem  29296  uvtx01vtx  29342  prcliscplgr  29359  cusgr0v  29373  vtxdg0e  29420  1loopgrvd2  29449  finsumvtxdg2ssteplem4  29494  finsumvtxdg2size  29496  isrgr  29505  fusgrregdegfi  29515  wspn0  29869  2wlkdlem8  29878  3wlkdlem8  30111  uhgr3cyclexlem  30125  1to2vfriswmgr  30223  1to3vfriswmgr  30224  frgrregorufr0  30268  frgrreg  30338  frgrregord013  30339  ex-ceil  30392  nmlno0lem  30737  minvecolem1  30818  hvsubeq0i  31007  hvsubaddi  31010  pjoc2i  31382  pjoml3i  31530  cmbr3i  31544  pjss2i  31624  hosubeq0i  31770  dmadjrnb  31850  nmlnop0iALT  31939  nmopcoadj0i  32047  stm1ri  32188  jplem2  32213  atoml2i  32327  chirredlem1  32334  cdj3lem3  32382  difininv  32461  disjnf  32514  disjpreima  32528  disjunsn  32538  f1od2  32663  wrdt2ind  32895  isunit2  33180  isdrng4  33234  lsmsnorb2  33329  ssdifidlprm  33395  fldext2chn  33695  zrhchr  33941  ddemeas  34203  braew  34209  aean  34211  eulerpartlemgh  34346  ballotlemfp1  34460  repr0  34579  hgt750lem2  34620  bnj1143  34757  nummin  35058  acycgr0v  35121  prclisacycgr  35124  cvmsss2  35247  cvmlift2lem13  35288  elrn3  35735  rankeq1o  36145  hfun  36152  bj-disj2r  37002  bj-sscon  37003  bj-0int  37075  bj-imdirco  37164  bj-pinftynminfty  37201  finxpreclem4  37368  nlpineqsn  37382  curunc  37582  tan2h  37592  poimirlem13  37613  poimirlem14  37614  poimirlem21  37621  poimirlem22  37622  asindmre  37683  totbndbnd  37769  rngosn3  37904  scott0f  38149  n0el2  38303  dfrel5  38314  dfrel6  38315  redundeq1  38606  dmqscoelseq  38639  dfeldisj5  38699  atbase  39268  llnbase  39488  lplnbase  39513  lvolbase  39557  lhpbase  39977  cdlemg31b0N  40673  cdlemg31b0a  40674  cdlemh  40796  sticksstones16  42135  sticksstones21  42140  unitscyglem3  42170  onsupmaxb  43212  iunrelexp0  43675  frege120  43956  clsk1indlem4  44017  gneispace  44107  scotteld  44219  undisjrab  44279  zfregs2VD  44814  dvnprod  45930  fnresfnco  47025  aiotavb  47074  afvpcfv0  47130  aovpcov0  47174  aov0ov0  47177  aovov0bi  47180  fnotaovb  47182  funressndmafv2rn  47207  fmtnoprmfac1lem  47548  lighneallem2  47590  stgrvtx0  47946  isubgr3stgrlem6  47955  pgnbgreunbgrlem2lem1  48098  pgnbgreunbgrlem2lem2  48099  pgnbgreunbgrlem2lem3  48100  snlindsntor  48456  rrx2pnedifcoorneorr  48702  itschlc0xyqsol1  48751  2itscp  48766  resinsn  48856  resinsnALT  48857  opndisj  48887  istermc  49459  lanrcl  49606  ranrcl  49607