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  3932  ssequn2  4152  ineqcom  4173  sseqin2  4186  dfss7  4214  dfss4  4232  rabeq0w  4350  rabeq0  4351  disj  4413  disjr  4414  undisj1  4425  undisj2  4426  undif  4445  undifr  4446  undifrOLD  4447  uneqdifeq  4456  rabeqsn  4631  reusn  4691  rabsneu  4693  eusn  4694  tppreqb  4769  elpreqpr  4831  uniintsn  4949  iin0  5317  dfepfr  5622  epfrc  5623  dmopab3  5883  dm0rn0  5888  rnopab3  5920  ssdmres  5984  iresn0n0  6025  imadisj  6051  args  6063  dffr3  6070  intirr  6091  dminxp  6153  dfrel3  6171  coeq0  6228  snres0  6271  sspred  6283  dffr4  6293  frpomin2  6314  frpoind  6315  cbviotavw  6472  fntpg  6576  fncnv  6589  mptfnf  6653  sbcfng  6685  f0rn0  6745  dff1o4  6808  dffv4  6855  tz6.12c  6880  fvun2  6953  fnreseql  7020  funopdmsn  7122  riota1  7365  riota2df  7367  riotaeqimp  7370  fnbrovb  7438  ovid  7530  ov  7533  ovg  7554  ovima0  7568  opiota  8038  frrlem13  8277  tz7.49c  8414  sucprcreg  9554  zfregfr  9558  inf3lem2  9582  zfregs2  9686  frind  9703  rankxpsuc  9835  scott0s  9841  cplem1  9842  cfslb2n  10221  fin23lem26  10278  dfacfin7  10352  axdc3lem4  10406  zorn2lem7  10455  alephom  10538  fpwwe2  10596  recmulnq  10917  recexsr  11060  map2psrpr  11063  renegcli  11483  addeq0  11601  elznn0  12544  xrsupss  13269  xrinfmss  13270  prinfzo0  13659  seqf1olem1  14006  seqf1olem2  14007  sqeqori  14179  hashrabsn1  14339  hashprb  14362  hashprdifel  14363  hashbclem  14417  hash2pwpr  14441  f1oun2prg  14883  modfsummods  15759  cshwrepswhash1  17073  ismgmid  18592  smndex2dnrinv  18842  oppgid  19288  lsmdisjr  19614  gexex  19783  gsumxp2  19910  dprd0  19963  oppr1  20259  opprunit  20286  zringndrg  21378  gsummoncoe1  22195  mat0dimcrng  22357  iinopn  22789  elcls  22960  ordthaus  23271  hauscmplem  23293  regr1lem2  23627  metdseq0  24743  minveclem1  25324  minveclem3b  25328  volun  25446  dyaddisj  25497  vieta1  26220  logeftb  26492  birthdaylem1  26861  dmgmaddn0  26933  gausslemma2d  27285  lgseisenlem1  27286  2lgslem4  27317  rpvmasum  27437  sltsolem1  27587  noinfbnd2lem1  27642  madeval2  27761  made0  27785  axsegconlem6  28849  edg0iedg0  28982  numedglnl  29071  ushgredgedg  29156  ushgredgedgloop  29158  uhgr0v0e  29165  usgr1v0edg  29184  usgrexmpllem  29187  usgr1v0e  29253  nbuhgr2vtx1edgblem  29278  uvtx01vtx  29324  prcliscplgr  29341  cusgr0v  29355  vtxdg0e  29402  1loopgrvd2  29431  finsumvtxdg2ssteplem4  29476  finsumvtxdg2size  29478  isrgr  29487  fusgrregdegfi  29497  wspn0  29854  2wlkdlem8  29863  3wlkdlem8  30096  uhgr3cyclexlem  30110  1to2vfriswmgr  30208  1to3vfriswmgr  30209  frgrregorufr0  30253  frgrreg  30323  frgrregord013  30324  ex-ceil  30377  nmlno0lem  30722  minvecolem1  30803  hvsubeq0i  30992  hvsubaddi  30995  pjoc2i  31367  pjoml3i  31515  cmbr3i  31529  pjss2i  31609  hosubeq0i  31755  dmadjrnb  31835  nmlnop0iALT  31924  nmopcoadj0i  32032  stm1ri  32173  jplem2  32198  atoml2i  32312  chirredlem1  32319  cdj3lem3  32367  difininv  32446  disjnf  32499  disjpreima  32513  disjunsn  32523  f1od2  32644  wrdt2ind  32875  isunit2  33191  isdrng4  33245  lsmsnorb2  33363  ssdifidlprm  33429  fldext2chn  33718  zrhchr  33964  ddemeas  34226  braew  34232  aean  34234  eulerpartlemgh  34369  ballotlemfp1  34483  repr0  34602  hgt750lem2  34643  bnj1143  34780  nummin  35081  acycgr0v  35135  prclisacycgr  35138  cvmsss2  35261  cvmlift2lem13  35302  elrn3  35749  rankeq1o  36159  hfun  36166  bj-disj2r  37016  bj-sscon  37017  bj-0int  37089  bj-imdirco  37178  bj-pinftynminfty  37215  finxpreclem4  37382  nlpineqsn  37396  curunc  37596  tan2h  37606  poimirlem13  37627  poimirlem14  37628  poimirlem21  37635  poimirlem22  37636  asindmre  37697  totbndbnd  37783  rngosn3  37918  scott0f  38163  n0el2  38317  dfrel5  38328  dfrel6  38329  redundeq1  38620  dmqscoelseq  38653  dfeldisj5  38713  atbase  39282  llnbase  39503  lplnbase  39528  lvolbase  39572  lhpbase  39992  cdlemg31b0N  40688  cdlemg31b0a  40689  cdlemh  40811  sticksstones16  42150  sticksstones21  42155  unitscyglem3  42185  onsupmaxb  43228  iunrelexp0  43691  frege120  43972  clsk1indlem4  44033  gneispace  44123  scotteld  44235  undisjrab  44295  zfregs2VD  44830  dvnprod  45947  fnresfnco  47042  aiotavb  47091  afvpcfv0  47147  aovpcov0  47191  aov0ov0  47194  aovov0bi  47197  fnotaovb  47199  funressndmafv2rn  47224  fmtnoprmfac1lem  47565  lighneallem2  47607  stgrvtx0  47961  isubgr3stgrlem6  47970  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  snlindsntor  48460  rrx2pnedifcoorneorr  48706  itschlc0xyqsol1  48755  2itscp  48770  resinsn  48860  resinsnALT  48861  opndisj  48891  istermc  49463  lanrcl  49610  ranrcl  49611