Theorem eqeq1i 2738

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

Syntax hints:   ↔ wb 205   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  eqeq12i  2751  eqabb  2874  neeq1i  3006  ssequn2  4184  ineqcom  4203  sseqin2  4216  dfss7  4241  dfss4  4259  rabeq0w  4384  rabeq0  4385  disj  4448  disjOLD  4449  disjr  4450  undisj1  4462  undisj2  4463  undif  4482  undifr  4483  undifrOLD  4484  uneqdifeq  4493  rabeqsn  4670  reusn  4732  rabsneu  4734  eusn  4735  tppreqb  4809  elpreqpr  4868  uniintsn  4992  iin0  5361  dfepfr  5662  epfrc  5663  dmopab3  5920  dm0rn0  5925  ssdmres  6005  iresn0n0  6054  imadisj  6080  args  6092  dffr3  6099  intirr  6120  dminxp  6180  dfrel3  6198  coeq0  6255  snres0  6298  sspred  6310  dffr4  6321  frpomin2  6343  frpoind  6344  tz6.26OLD  6350  wfiOLD  6353  cbviotavw  6504  fntpg  6609  fncnv  6622  mptfnf  6686  sbcfng  6715  f0rn0  6777  dff1o4  6842  dffv4  6889  tz6.12c  6914  fvun2  6984  fnreseql  7050  funopdmsn  7148  riota1  7387  riota2df  7389  riotaeqimp  7392  fnbrovb  7458  ovid  7549  ov  7552  ovg  7572  ovima0  7586  opiota  8045  frrlem13  8283  wfrlem8OLD  8316  tz7.49c  8446  sucprcreg  9596  zfregfr  9600  inf3lem2  9624  zfregs2  9728  frind  9745  rankxpsuc  9877  scott0s  9883  cplem1  9884  cfslb2n  10263  fin23lem26  10320  dfacfin7  10394  axdc3lem4  10448  zorn2lem7  10497  alephom  10580  fpwwe2  10638  recmulnq  10959  recexsr  11102  map2psrpr  11105  renegcli  11521  addeq0  11637  elznn0  12573  xrsupss  13288  xrinfmss  13289  prinfzo0  13671  seqf1olem1  14007  seqf1olem2  14008  sqeqori  14178  hashrabsn1  14334  hashprb  14357  hashprdifel  14358  hashbclem  14411  hash2pwpr  14437  f1oun2prg  14868  modfsummods  15739  cshwrepswhash1  17036  ismgmid  18584  smndex2dnrinv  18796  oppgid  19223  lsmdisjr  19552  gexex  19721  gsumxp2  19848  dprd0  19901  oppr1  20164  opprunit  20191  opprdomn  20919  zringndrg  21038  gsummoncoe1  21828  mat0dimcrng  21972  iinopn  22404  elcls  22577  ordthaus  22888  hauscmplem  22910  regr1lem2  23244  metdseq0  24370  minveclem1  24941  minveclem3b  24945  volun  25062  dyaddisj  25113  vieta1  25825  logeftb  26092  birthdaylem1  26456  dmgmaddn0  26527  gausslemma2d  26877  lgseisenlem1  26878  2lgslem4  26909  rpvmasum  27029  sltsolem1  27178  noinfbnd2lem1  27233  madeval2  27349  made0  27369  axsegconlem6  28211  edg0iedg0  28346  numedglnl  28435  ushgredgedg  28517  ushgredgedgloop  28519  uhgr0v0e  28526  usgr1v0edg  28545  usgrexmpllem  28548  usgr1v0e  28614  nbuhgr2vtx1edgblem  28639  uvtx01vtx  28685  prcliscplgr  28702  cusgr0v  28716  vtxdg0e  28762  1loopgrvd2  28791  finsumvtxdg2ssteplem4  28836  finsumvtxdg2size  28838  isrgr  28847  fusgrregdegfi  28857  wspn0  29209  2wlkdlem8  29218  3wlkdlem8  29451  uhgr3cyclexlem  29465  1to2vfriswmgr  29563  1to3vfriswmgr  29564  frgrregorufr0  29608  frgrreg  29678  frgrregord013  29679  ex-ceil  29732  nmlno0lem  30077  minvecolem1  30158  hvsubeq0i  30347  hvsubaddi  30350  pjoc2i  30722  pjoml3i  30870  cmbr3i  30884  pjss2i  30964  hosubeq0i  31110  dmadjrnb  31190  nmlnop0iALT  31279  nmopcoadj0i  31387  stm1ri  31528  jplem2  31553  atoml2i  31667  chirredlem1  31674  cdj3lem3  31722  difininv  31786  disjnf  31832  disjpreima  31846  disjunsn  31856  f1od2  31977  wrdt2ind  32148  isdrng4  32426  lsmsnorb2  32533  zrhchr  32987  ddemeas  33265  braew  33271  aean  33273  eulerpartlemgh  33408  ballotlemfp1  33521  repr0  33654  hgt750lem2  33695  bnj1143  33832  nummin  34125  acycgr0v  34170  prclisacycgr  34173  cvmsss2  34296  cvmlift2lem13  34337  elrn3  34763  rankeq1o  35174  hfun  35181  bj-disj2r  35957  bj-sscon  35958  bj-0int  36030  bj-imdirco  36119  bj-pinftynminfty  36156  finxpreclem4  36323  nlpineqsn  36337  curunc  36518  tan2h  36528  poimirlem13  36549  poimirlem14  36550  poimirlem21  36557  poimirlem22  36558  asindmre  36619  totbndbnd  36705  rngosn3  36840  scott0f  37085  n0el2  37250  dfrel5  37263  dfrel6  37264  redundeq1  37547  dmqscoelseq  37579  dfeldisj5  37639  atbase  38207  llnbase  38428  lplnbase  38453  lvolbase  38497  lhpbase  38917  cdlemg31b0N  39613  cdlemg31b0a  39614  cdlemh  39736  sticksstones16  41026  sticksstones21  41031  metakunt24  41056  onsupmaxb  42036  iunrelexp0  42501  frege120  42782  clsk1indlem4  42843  gneispace  42933  scotteld  43053  undisjrab  43113  zfregs2VD  43650  dvnprod  44713  fnresfnco  45799  aiotavb  45846  afvpcfv0  45902  aovpcov0  45946  aov0ov0  45949  aovov0bi  45952  fnotaovb  45954  funressndmafv2rn  45979  fmtnoprmfac1lem  46280  lighneallem2  46322  snlindsntor  47200  rrx2pnedifcoorneorr  47451  itschlc0xyqsol1  47500  2itscp  47515  opndisj  47583