Theorem eqeq1i 2774

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

Syntax hints:   ↔ wb 209   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqeq12i  2787  eqabb  2908  neeq1i  3028  dfss2  3931  ssequn2  4150  ineqcom  4171  dfss7  4212  dfss4  4230  rabeq0w  4351  rabeq0  4352  disj  4416  undisj1  4428  undisj2  4429  undif  4448  undifr  4449  rabeqsn  4638  reusn  4698  rabsneu  4700  eusn  4701  tppreqb  4777  elpreqpr  4836  uniintsn  4954  iin0  5334  dfepfr  5646  epfrc  5647  dmopab3  5910  dm0rn0  5915  dm0rn0OLD  5916  rnopab3  5947  ssdmres  6013  iresn0n0  6057  imadisj  6083  args  6095  dffr3  6102  intirr  6119  dminxp  6179  dfrel3  6198  coeq0  6258  snres0  6300  sspred  6312  dffr4  6322  frpomin2  6343  frpoind  6344  cbviotavw  6501  fntpg  6597  fncnv  6610  mptfnf  6671  sbcfng  6703  f0rn0  6764  dff1o4  6830  dffv4  6879  tz6.12c  6904  fvun2  6974  fnreseql  7044  funopdmsn  7148  riota1  7389  riota2df  7391  riotaeqimp  7394  fnbrovb  7462  ovid  7552  ov  7555  ovg  7576  ovima0  7590  opiota  8055  frrlem13  8294  tz7.49c  8432  sucprcreg  9567  sucprcregOLD  9568  zfregfr  9572  inf3lem2  9597  zfregs2  9701  frind  9721  rankxpsuc  9853  scott0s  9861  scotteld  9871  cplem1  9874  cfslb2n  10251  fin23lem26  10308  dfacfin7  10382  axdc3lem4  10436  zorn2lem7  10485  alephom  10569  fpwwe2  10627  recmulnq  10948  recexsr  11091  map2psrpr  11094  renegcli  11518  addeq0  11636  elznn0  12605  xrsupss  13334  xrinfmss  13335  prinfzo0  13726  seqf1olem1  14076  seqf1olem2  14077  sqeqori  14249  hashrabsn1  14409  hashprb  14432  hashprdifel  14433  hashbclem  14488  hash2pwpr  14512  f1oun2prg  14953  modfsummods  15844  cshwrepswhash1  17161  ismgmid  18722  smndex2dnrinv  18976  oppgid  19425  lsmdisjr  19753  gexex  19922  gsumxp2  20049  dprd0  20102  oppr1  20431  opprunit  20458  ssdifidlprm  21454  zringndrg  21586  gsummoncoe1  22436  mat0dimcrng  22595  iinopn  23027  elcls  23198  ordthaus  23509  hauscmplem  23531  regr1lem2  23865  metdseq0  24980  minveclem1  25551  minveclem3b  25555  volun  25672  dyaddisj  25723  vieta1  26441  logeftb  26713  birthdaylem1  27081  dmgmaddn0  27152  gausslemma2d  27503  lgseisenlem1  27504  2lgslem4  27535  rpvmasum  27655  ltssolem1  27804  noinfbnd2lem1  27859  madeval2  27991  made0  28021  axsegconlem6  29212  edg0iedg0  29345  numedglnl  29434  ushgredgedg  29519  ushgredgedgloop  29521  uhgr0v0e  29528  usgr1v0edg  29547  usgrexmpllem  29550  usgr1v0e  29616  nbuhgr2vtx1edgblem  29641  uvtx01vtx  29687  prcliscplgr  29704  cusgr0v  29718  vtxdg0e  29764  1loopgrvd2  29793  finsumvtxdg2ssteplem4  29838  finsumvtxdg2size  29840  isrgr  29849  fusgrregdegfi  29859  wspn0  30213  2wlkdlem8  30222  3wlkdlem8  30458  uhgr3cyclexlem  30472  1to2vfriswmgr  30570  1to3vfriswmgr  30571  frgrregorufr0  30615  frgrreg  30685  frgrregord013  30686  ex-ceil  30739  nmlno0lem  31085  minvecolem1  31166  hvsubeq0i  31355  hvsubaddi  31358  pjoc2i  31730  pjoml3i  31878  cmbr3i  31892  pjss2i  31972  hosubeq0i  32118  dmadjrnb  32198  nmlnop0iALT  32287  nmopcoadj0i  32395  stm1ri  32536  jplem2  32561  atoml2i  32675  chirredlem1  32682  cdj3lem3  32730  difininv  32803  disjnf  32855  disjpreima  32869  disjunsn  32879  f1od2  33004  wrdt2ind  33213  isunit2  33499  isdrng4  33558  lsmsnorb2  33648  fldext2chn  34062  zrhchr  34308  ddemeas  34570  braew  34576  aean  34578  eulerpartlemgh  34712  ballotlemfp1  34826  repr0  34942  hgt750lem2  34983  bnj1143  35122  nummin  35426  acycgr0v  35538  prclisacycgr  35541  cvmsss2  35664  cvmlift2lem13  35705  elrn3  36152  rankeq1o  36561  hfun  36568  bj-disj2r  37551  bj-sscon  37552  bj-0int  37630  bj-imdirco  37721  bj-pinftynminfty  37758  finxpreclem4  37927  nlpineqsn  37941  curunc  38140  tan2h  38150  poimirlem13  38171  poimirlem14  38172  poimirlem21  38179  poimirlem22  38180  asindmre  38241  totbndbnd  38327  rngosn3  38462  scott0f  38707  n0el2  38873  dfrel5  38884  dfrel6  38885  redundeq1  39251  dmqscoelseq  39284  dfeldisj5  39351  atbase  39952  llnbase  40172  lplnbase  40197  lvolbase  40241  lhpbase  40661  cdlemg31b0N  41357  cdlemg31b0a  41358  cdlemh  41480  sticksstones16  42818  sticksstones21  42823  unitscyglem3  42853  onsupmaxb  43857  iunrelexp0  44319  frege120  44600  clsk1indlem4  44661  gneispace  44751  undisjrab  44907  zfregs2VD  45440  dvnprod  46554  fnresfnco  47666  aiotavb  47715  afvpcfv0  47771  aovpcov0  47815  aov0ov0  47818  aovov0bi  47821  fnotaovb  47823  funressndmafv2rn  47848  fmtnoprmfac1lem  48204  lighneallem2  48246  stgrvtx0  48615  isubgr3stgrlem6  48624  pgnbgreunbgrlem2lem1  48767  pgnbgreunbgrlem2lem2  48768  pgnbgreunbgrlem2lem3  48769  snlindsntor  49135  rrx2pnedifcoorneorr  49381  itschlc0xyqsol1  49430  2itscp  49445  resinsn  49534  resinsnALT  49535  opndisj  49565  istermc  50136  lanrcl  50283  ranrcl  50284