Theorem eqeq1i 2735

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 2734	. 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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  eqeq12i  2748  eqabb  2868  neeq1i  2990  dfss2  3935  ssequn2  4155  ineqcom  4176  sseqin2  4189  dfss7  4217  dfss4  4235  rabeq0w  4353  rabeq0  4354  disj  4416  disjr  4417  undisj1  4428  undisj2  4429  undif  4448  undifr  4449  undifrOLD  4450  uneqdifeq  4459  rabeqsn  4634  reusn  4694  rabsneu  4696  eusn  4697  tppreqb  4772  elpreqpr  4834  uniintsn  4952  iin0  5320  dfepfr  5625  epfrc  5626  dmopab3  5886  dm0rn0  5891  rnopab3  5923  ssdmres  5987  iresn0n0  6028  imadisj  6054  args  6066  dffr3  6073  intirr  6094  dminxp  6156  dfrel3  6174  coeq0  6231  snres0  6274  sspred  6286  dffr4  6296  frpomin2  6317  frpoind  6318  cbviotavw  6475  fntpg  6579  fncnv  6592  mptfnf  6656  sbcfng  6688  f0rn0  6748  dff1o4  6811  dffv4  6858  tz6.12c  6883  fvun2  6956  fnreseql  7023  funopdmsn  7125  riota1  7368  riota2df  7370  riotaeqimp  7373  fnbrovb  7441  ovid  7533  ov  7536  ovg  7557  ovima0  7571  opiota  8041  frrlem13  8280  tz7.49c  8417  sucprcreg  9561  zfregfr  9565  inf3lem2  9589  zfregs2  9693  frind  9710  rankxpsuc  9842  scott0s  9848  cplem1  9849  cfslb2n  10228  fin23lem26  10285  dfacfin7  10359  axdc3lem4  10413  zorn2lem7  10462  alephom  10545  fpwwe2  10603  recmulnq  10924  recexsr  11067  map2psrpr  11070  renegcli  11490  addeq0  11608  elznn0  12551  xrsupss  13276  xrinfmss  13277  prinfzo0  13666  seqf1olem1  14013  seqf1olem2  14014  sqeqori  14186  hashrabsn1  14346  hashprb  14369  hashprdifel  14370  hashbclem  14424  hash2pwpr  14448  f1oun2prg  14890  modfsummods  15766  cshwrepswhash1  17080  ismgmid  18599  smndex2dnrinv  18849  oppgid  19295  lsmdisjr  19621  gexex  19790  gsumxp2  19917  dprd0  19970  oppr1  20266  opprunit  20293  zringndrg  21385  gsummoncoe1  22202  mat0dimcrng  22364  iinopn  22796  elcls  22967  ordthaus  23278  hauscmplem  23300  regr1lem2  23634  metdseq0  24750  minveclem1  25331  minveclem3b  25335  volun  25453  dyaddisj  25504  vieta1  26227  logeftb  26499  birthdaylem1  26868  dmgmaddn0  26940  gausslemma2d  27292  lgseisenlem1  27293  2lgslem4  27324  rpvmasum  27444  sltsolem1  27594  noinfbnd2lem1  27649  madeval2  27768  made0  27792  axsegconlem6  28856  edg0iedg0  28989  numedglnl  29078  ushgredgedg  29163  ushgredgedgloop  29165  uhgr0v0e  29172  usgr1v0edg  29191  usgrexmpllem  29194  usgr1v0e  29260  nbuhgr2vtx1edgblem  29285  uvtx01vtx  29331  prcliscplgr  29348  cusgr0v  29362  vtxdg0e  29409  1loopgrvd2  29438  finsumvtxdg2ssteplem4  29483  finsumvtxdg2size  29485  isrgr  29494  fusgrregdegfi  29504  wspn0  29861  2wlkdlem8  29870  3wlkdlem8  30103  uhgr3cyclexlem  30117  1to2vfriswmgr  30215  1to3vfriswmgr  30216  frgrregorufr0  30260  frgrreg  30330  frgrregord013  30331  ex-ceil  30384  nmlno0lem  30729  minvecolem1  30810  hvsubeq0i  30999  hvsubaddi  31002  pjoc2i  31374  pjoml3i  31522  cmbr3i  31536  pjss2i  31616  hosubeq0i  31762  dmadjrnb  31842  nmlnop0iALT  31931  nmopcoadj0i  32039  stm1ri  32180  jplem2  32205  atoml2i  32319  chirredlem1  32326  cdj3lem3  32374  difininv  32453  disjnf  32506  disjpreima  32520  disjunsn  32530  f1od2  32651  wrdt2ind  32882  isunit2  33198  isdrng4  33252  lsmsnorb2  33370  ssdifidlprm  33436  fldext2chn  33725  zrhchr  33971  ddemeas  34233  braew  34239  aean  34241  eulerpartlemgh  34376  ballotlemfp1  34490  repr0  34609  hgt750lem2  34650  bnj1143  34787  nummin  35088  acycgr0v  35142  prclisacycgr  35145  cvmsss2  35268  cvmlift2lem13  35309  elrn3  35756  rankeq1o  36166  hfun  36173  bj-disj2r  37023  bj-sscon  37024  bj-0int  37096  bj-imdirco  37185  bj-pinftynminfty  37222  finxpreclem4  37389  nlpineqsn  37403  curunc  37603  tan2h  37613  poimirlem13  37634  poimirlem14  37635  poimirlem21  37642  poimirlem22  37643  asindmre  37704  totbndbnd  37790  rngosn3  37925  scott0f  38170  n0el2  38324  dfrel5  38335  dfrel6  38336  redundeq1  38627  dmqscoelseq  38660  dfeldisj5  38720  atbase  39289  llnbase  39510  lplnbase  39535  lvolbase  39579  lhpbase  39999  cdlemg31b0N  40695  cdlemg31b0a  40696  cdlemh  40818  sticksstones16  42157  sticksstones21  42162  unitscyglem3  42192  onsupmaxb  43235  iunrelexp0  43698  frege120  43979  clsk1indlem4  44040  gneispace  44130  scotteld  44242  undisjrab  44302  zfregs2VD  44837  dvnprod  45954  fnresfnco  47046  aiotavb  47095  afvpcfv0  47151  aovpcov0  47195  aov0ov0  47198  aovov0bi  47201  fnotaovb  47203  funressndmafv2rn  47228  fmtnoprmfac1lem  47569  lighneallem2  47611  stgrvtx0  47965  isubgr3stgrlem6  47974  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  snlindsntor  48464  rrx2pnedifcoorneorr  48710  itschlc0xyqsol1  48759  2itscp  48774  resinsn  48864  resinsnALT  48865  opndisj  48895  istermc  49467  lanrcl  49614  ranrcl  49615