Theorem eqeq1i 2741

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

Syntax hints:   ↔ wb 209   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728

This theorem is referenced by:  eqeq12i  2751  neeq1i  2996  ssequn2  4083  ineqcom  4103  sseqin2  4116  dfss7  4141  dfss4  4159  rabeq0w  4284  rabeq0  4285  disj  4348  disjOLD  4349  disjr  4350  undisj1  4362  undisj2  4363  undif  4382  uneqdifeq  4390  rabeqsn  4568  reusn  4629  rabsneu  4631  eusn  4632  tppreqb  4704  elpreqpr  4763  uniintsn  4884  iin0  5238  dfepfr  5521  epfrc  5522  dmopab3  5773  dm0rn0  5779  ssdmres  5859  iresn0n0  5908  imadisj  5933  args  5942  dffr3  5947  intirr  5963  dminxp  6023  dfrel3  6041  coeq0  6099  sspred  6148  dffr4  6156  frpomin2  6173  frpoind  6174  tz6.26  6179  wfi  6181  unisuc  6267  cbviotavw  6324  fntpg  6418  fncnv  6431  mptfnf  6491  sbcfng  6520  f0rn0  6582  dff1o4  6647  dffv4  6692  fvun2  6781  fnreseql  6846  funopdmsn  6943  f1ofvswap  7094  riota1  7170  riota2df  7172  riotaeqimp  7175  fnbrovb  7240  ovid  7328  ov  7331  ovg  7351  ovima0  7365  opiota  7807  frrlem13  8017  wfrlem8  8040  tz7.49c  8160  sucprcreg  9195  zfregfr  9198  inf3lem2  9222  zfregs2  9327  rankxpsuc  9463  scott0s  9469  cplem1  9470  cfslb2n  9847  fin23lem26  9904  dfacfin7  9978  axdc3lem4  10032  zorn2lem7  10081  alephom  10164  fpwwe2  10222  recmulnq  10543  recexsr  10686  map2psrpr  10689  renegcli  11104  addeq0  11220  elznn0  12156  xrsupss  12864  xrinfmss  12865  prinfzo0  13246  seqf1olem1  13580  seqf1olem2  13581  sqeqori  13747  hashrabsn1  13906  hashprb  13929  hashprdifel  13930  hashbclem  13981  hash2pwpr  14007  f1oun2prg  14447  modfsummods  15320  cshwrepswhash1  16619  ismgmid  18091  smndex2dnrinv  18296  oppgid  18702  lsmdisjr  19028  gexex  19192  gsumxp2  19319  dprd0  19372  oppr1  19606  opprunit  19633  opprdomn  20293  zringndrg  20409  gsummoncoe1  21179  mat0dimcrng  21321  iinopn  21753  elcls  21924  ordthaus  22235  hauscmplem  22257  regr1lem2  22591  metdseq0  23705  minveclem1  24275  minveclem3b  24279  volun  24396  dyaddisj  24447  vieta1  25159  logeftb  25426  birthdaylem1  25788  dmgmaddn0  25859  gausslemma2d  26209  lgseisenlem1  26210  2lgslem4  26241  rpvmasum  26361  axsegconlem6  26967  edg0iedg0  27100  numedglnl  27189  ushgredgedg  27271  ushgredgedgloop  27273  uhgr0v0e  27280  usgr1v0edg  27299  usgrexmpllem  27302  usgr1v0e  27368  nbuhgr2vtx1edgblem  27393  uvtx01vtx  27439  prcliscplgr  27456  cusgr0v  27470  vtxdg0e  27516  1loopgrvd2  27545  finsumvtxdg2ssteplem4  27590  finsumvtxdg2size  27592  isrgr  27601  fusgrregdegfi  27611  wspn0  27962  2wlkdlem8  27971  3wlkdlem8  28204  uhgr3cyclexlem  28218  1to2vfriswmgr  28316  1to3vfriswmgr  28317  frgrregorufr0  28361  frgrreg  28431  frgrregord013  28432  ex-ceil  28485  nmlno0lem  28828  minvecolem1  28909  hvsubeq0i  29098  hvsubaddi  29101  pjoc2i  29473  pjoml3i  29621  cmbr3i  29635  pjss2i  29715  hosubeq0i  29861  dmadjrnb  29941  nmlnop0iALT  30030  nmopcoadj0i  30138  stm1ri  30279  jplem2  30304  atoml2i  30418  chirredlem1  30425  cdj3lem3  30473  difininv  30537  undifr  30545  disjnf  30582  disjpreima  30596  disjunsn  30606  f1od2  30730  wrdt2ind  30899  lsmsnorb2  31248  zrhchr  31592  ddemeas  31870  braew  31876  aean  31878  eulerpartlemgh  32011  ballotlemfp1  32124  repr0  32257  hgt750lem2  32298  bnj1143  32437  nummin  32730  acycgr0v  32777  prclisacycgr  32780  cvmsss2  32903  cvmlift2lem13  32944  snres0  33344  elrn3  33399  frind  33460  sltsolem1  33564  noinfbnd2lem1  33619  madeval2  33723  made0  33743  rankeq1o  34159  hfun  34166  bj-disj2r  34904  bj-sscon  34905  bj-0int  34956  bj-imdirco  35045  bj-pinftynminfty  35082  finxpreclem4  35251  nlpineqsn  35265  curunc  35445  tan2h  35455  poimirlem13  35476  poimirlem14  35477  poimirlem21  35484  poimirlem22  35485  asindmre  35546  totbndbnd  35633  rngosn3  35768  scott0f  36013  n0el2  36154  dfrel5  36167  dfrel6  36168  redundeq1  36428  dmqscoelseq  36459  dfeldisj5  36518  atbase  36989  llnbase  37209  lplnbase  37234  lvolbase  37278  lhpbase  37698  cdlemg31b0N  38394  cdlemg31b0a  38395  cdlemh  38517  sticksstones16  39787  metakunt24  39811  iunrelexp0  40928  frege120  41209  clsk1indlem4  41272  gneispace  41362  scotteld  41478  undisjrab  41538  zfregs2VD  42075  dvnprod  43108  fnresfnco  44150  aiotavb  44197  afvpcfv0  44253  aovpcov0  44297  aov0ov0  44300  aovov0bi  44303  fnotaovb  44305  funressndmafv2rn  44330  fmtnoprmfac1lem  44632  lighneallem2  44674  snlindsntor  45428  rrx2pnedifcoorneorr  45679  itschlc0xyqsol1  45728  2itscp  45743  opndisj  45812