Theorem eqeq1i 2768

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

Syntax hints:   ↔ wb 209   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqeq12i  2781  eqabb  2902  neeq1i  3022  dfss2  3923  ssequn2  4142  ineqcom  4163  dfss7  4204  dfss4  4222  inssdif0  4329  rabeq0w  4344  rabeq0  4345  disj  4410  undisj1  4422  undisj2  4423  undif  4443  undifr  4444  rabeqsn  4633  reusn  4693  rabsneu  4695  eusn  4696  tppreqb  4773  elpreqpr  4832  uniintsn  4950  iin0  5333  dfepfr  5645  epfrc  5646  dmopab3  5909  dm0rn0  5914  dm0rn0OLD  5915  rnopab3  5946  ssdmres  6012  iresn0n0  6056  imadisj  6082  args  6094  dffr3  6101  intirr  6118  dminxp  6178  dfrel3  6197  coeq0  6257  snres0  6299  sspred  6311  dffr4  6321  frpomin2  6342  frpoind  6343  cbviotavw  6500  fntpg  6596  fncnv  6609  mptfnf  6670  sbcfng  6702  f0rn0  6763  dff1o4  6829  dffv4  6878  tz6.12c  6903  fvun2  6973  fnreseql  7043  funopdmsn  7147  riota1  7388  riota2df  7390  riotaeqimp  7393  fnbrovb  7461  ovid  7551  ov  7554  ovg  7575  ovima0  7589  opiota  8052  frrlem13  8291  tz7.49c  8429  sucprcreg  9564  sucprcregOLD  9565  zfregfr  9569  inf3lem2  9594  zfregs2  9698  frind  9718  rankxpsuc  9850  scott0s  9858  scotteld  9868  cplem1  9871  cfslb2n  10247  fin23lem26  10304  dfacfin7  10378  axdc3lem4  10432  zorn2lem7  10481  alephom  10565  fpwwe2  10623  recmulnq  10944  recexsr  11087  map2psrpr  11090  renegcli  11514  addeq0  11632  elznn0  12601  xrsupss  13330  xrinfmss  13331  prinfzo0  13723  seqf1olem1  14073  seqf1olem2  14074  sqeqori  14246  hashrabsn1  14406  hashprb  14429  hashprdifel  14430  hashbclem  14485  hash2pwpr  14509  f1oun2prg  14950  modfsummods  15841  cshwrepswhash1  17157  ismgmid  18718  smndex2dnrinv  18972  oppgid  19421  lsmdisjr  19749  gexex  19918  gsumxp2  20045  dprd0  20098  oppr1  20428  opprunit  20455  isdrng4  20839  isdrng3lem1  20851  ssdifidlprm  21486  zringndrg  21618  gsummoncoe1  22468  mat0dimcrng  22627  iinopn  23059  elcls  23230  ordthaus  23541  hauscmplem  23563  regr1lem2  23897  metdseq0  25012  minveclem1  25583  minveclem3b  25587  volun  25704  dyaddisj  25755  vieta1  26473  logeftb  26748  birthdaylem1  27116  dmgmaddn0  27187  gausslemma2d  27538  lgseisenlem1  27539  2lgslem4  27570  rpvmasum  27690  ltssolem1  27839  noinfbnd2lem1  27894  madeval2  28026  made0  28056  axsegconlem6  29272  edg0iedg0  29405  numedglnl  29494  ushgredgedg  29579  ushgredgedgloop  29581  uhgr0v0e  29588  usgr1v0edg  29607  usgrexmpllem  29610  usgr1v0e  29676  nbuhgr2vtx1edgblem  29701  uvtx01vtx  29747  prcliscplgr  29764  cusgr0v  29778  vtxdg0e  29824  1loopgrvd2  29853  finsumvtxdg2ssteplem4  29898  finsumvtxdg2size  29900  isrgr  29909  fusgrregdegfi  29919  wspn0  30273  2wlkdlem8  30282  3wlkdlem8  30518  uhgr3cyclexlem  30532  1to2vfriswmgr  30630  1to3vfriswmgr  30631  frgrregorufr0  30675  frgrreg  30745  frgrregord013  30746  ex-ceil  30799  nmlno0lem  31145  minvecolem1  31226  hvsubeq0i  31415  hvsubaddi  31418  pjoc2i  31790  pjoml3i  31938  cmbr3i  31952  pjss2i  32032  hosubeq0i  32178  dmadjrnb  32258  nmlnop0iALT  32347  nmopcoadj0i  32455  stm1ri  32596  jplem2  32621  atoml2i  32735  chirredlem1  32742  cdj3lem3  32790  difininv  32863  disjnf  32915  disjpreima  32929  disjunsn  32939  f1od2  33064  wrdt2ind  33273  isunit2  33559  lsmsnorb2  33705  fldext2chn  34118  zrhchr  34364  ddemeas  34626  braew  34632  aean  34634  eulerpartlemgh  34768  ballotlemfp1  34882  repr0  34998  hgt750lem2  35039  bnj1143  35178  nummin  35484  scott0b  35521  acycgr0v  35640  prclisacycgr  35643  cvmsss2  35766  cvmlift2lem13  35807  elrn3  36254  rankeq1o  36663  hfun  36670  bj-disj2r  37664  bj-sscon  37665  bj-0int  37743  bj-imdirco  37834  bj-pinftynminfty  37871  finxpreclem4  38040  nlpineqsn  38054  curunc  38253  tan2h  38263  poimirlem13  38284  poimirlem14  38285  poimirlem21  38292  poimirlem22  38293  asindmre  38354  totbndbnd  38440  rngosn3  38575  scott0f  38818  n0el2  38984  dfrel5  38995  dfrel6  38996  redundeq1  39362  dmqscoelseq  39395  dfeldisj5  39462  atbase  40063  llnbase  40283  lplnbase  40308  lvolbase  40352  lhpbase  40772  cdlemg31b0N  41468  cdlemg31b0a  41469  cdlemh  41591  sticksstones16  42929  sticksstones21  42934  unitscyglem3  42964  onsupmaxb  43966  iunrelexp0  44428  frege120  44709  clsk1indlem4  44770  gneispace  44860  undisjrab  45016  zfregs2VD  45549  dvnprod  46663  fnresfnco  47778  aiotavb  47827  afvpcfv0  47883  aovpcov0  47927  aov0ov0  47930  aovov0bi  47933  fnotaovb  47935  funressndmafv2rn  47960  fmtnoprmfac1lem  48316  lighneallem2  48358  stgrvtx0  48727  isubgr3stgrlem6  48736  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  snlindsntor  49251  rrx2pnedifcoorneorr  49497  itschlc0xyqsol1  49546  2itscp  49561  resinsn  49650  resinsnALT  49651  opndisj  49681  istermc  50252  lanrcl  50399  ranrcl  50400