Theorem eqeq1i 2742

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

Syntax hints:   ↔ wb 206   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  eqeq12i  2755  eqabb  2876  neeq1i  2997  dfss2  3920  ssequn2  4142  ineqcom  4163  sseqin2  4176  dfss7  4204  dfss4  4222  rabeq0w  4340  rabeq0  4341  disj  4403  disjr  4404  undisj1  4415  undisj2  4416  undif  4435  undifr  4436  undifrOLD  4437  uneqdifeq  4446  rabeqsn  4625  reusn  4685  rabsneu  4687  eusn  4688  tppreqb  4762  elpreqpr  4824  uniintsn  4941  iin0  5308  dfepfr  5609  epfrc  5610  dmopab3  5869  dm0rn0  5874  dm0rn0OLD  5875  rnopab3  5906  ssdmres  5973  iresn0n0  6014  imadisj  6040  args  6052  dffr3  6059  intirr  6076  dminxp  6139  dfrel3  6157  coeq0  6215  snres0  6257  sspred  6269  dffr4  6279  frpomin2  6300  frpoind  6301  cbviotavw  6457  fntpg  6553  fncnv  6566  mptfnf  6628  sbcfng  6660  f0rn0  6720  dff1o4  6783  dffv4  6832  tz6.12c  6857  fvun2  6927  fnreseql  6995  funopdmsn  7097  riota1  7338  riota2df  7340  riotaeqimp  7343  fnbrovb  7411  ovid  7501  ov  7504  ovg  7525  ovima0  7539  opiota  8005  frrlem13  8242  tz7.49c  8379  sucprcreg  9513  zfregfr  9517  inf3lem2  9542  zfregs2  9646  frind  9666  rankxpsuc  9798  scott0s  9804  cplem1  9805  cfslb2n  10182  fin23lem26  10239  dfacfin7  10313  axdc3lem4  10367  zorn2lem7  10416  alephom  10500  fpwwe2  10558  recmulnq  10879  recexsr  11022  map2psrpr  11025  renegcli  11446  addeq0  11564  elznn0  12507  xrsupss  13228  xrinfmss  13229  prinfzo0  13618  seqf1olem1  13968  seqf1olem2  13969  sqeqori  14141  hashrabsn1  14301  hashprb  14324  hashprdifel  14325  hashbclem  14379  hash2pwpr  14403  f1oun2prg  14844  modfsummods  15720  cshwrepswhash1  17034  ismgmid  18594  smndex2dnrinv  18844  oppgid  19289  lsmdisjr  19617  gexex  19786  gsumxp2  19913  dprd0  19966  oppr1  20290  opprunit  20317  zringndrg  21427  gsummoncoe1  22256  mat0dimcrng  22418  iinopn  22850  elcls  23021  ordthaus  23332  hauscmplem  23354  regr1lem2  23688  metdseq0  24803  minveclem1  25384  minveclem3b  25388  volun  25506  dyaddisj  25557  vieta1  26280  logeftb  26552  birthdaylem1  26921  dmgmaddn0  26993  gausslemma2d  27345  lgseisenlem1  27346  2lgslem4  27377  rpvmasum  27497  sltsolem1  27647  noinfbnd2lem1  27702  madeval2  27831  made0  27855  axsegconlem6  28978  edg0iedg0  29111  numedglnl  29200  ushgredgedg  29285  ushgredgedgloop  29287  uhgr0v0e  29294  usgr1v0edg  29313  usgrexmpllem  29316  usgr1v0e  29382  nbuhgr2vtx1edgblem  29407  uvtx01vtx  29453  prcliscplgr  29470  cusgr0v  29484  vtxdg0e  29531  1loopgrvd2  29560  finsumvtxdg2ssteplem4  29605  finsumvtxdg2size  29607  isrgr  29616  fusgrregdegfi  29626  wspn0  29980  2wlkdlem8  29989  3wlkdlem8  30225  uhgr3cyclexlem  30239  1to2vfriswmgr  30337  1to3vfriswmgr  30338  frgrregorufr0  30382  frgrreg  30452  frgrregord013  30453  ex-ceil  30506  nmlno0lem  30851  minvecolem1  30932  hvsubeq0i  31121  hvsubaddi  31124  pjoc2i  31496  pjoml3i  31644  cmbr3i  31658  pjss2i  31738  hosubeq0i  31884  dmadjrnb  31964  nmlnop0iALT  32053  nmopcoadj0i  32161  stm1ri  32302  jplem2  32327  atoml2i  32441  chirredlem1  32448  cdj3lem3  32496  difininv  32574  disjnf  32627  disjpreima  32641  disjunsn  32651  f1od2  32779  wrdt2ind  33016  isunit2  33303  isdrng4  33358  lsmsnorb2  33454  ssdifidlprm  33520  fldext2chn  33866  zrhchr  34112  ddemeas  34374  braew  34380  aean  34382  eulerpartlemgh  34516  ballotlemfp1  34630  repr0  34749  hgt750lem2  34790  bnj1143  34927  nummin  35230  acycgr0v  35323  prclisacycgr  35326  cvmsss2  35449  cvmlift2lem13  35490  elrn3  35937  rankeq1o  36346  hfun  36353  bj-disj2r  37204  bj-sscon  37205  bj-0int  37277  bj-imdirco  37366  bj-pinftynminfty  37403  finxpreclem4  37570  nlpineqsn  37584  curunc  37774  tan2h  37784  poimirlem13  37805  poimirlem14  37806  poimirlem21  37813  poimirlem22  37814  asindmre  37875  totbndbnd  37961  rngosn3  38096  scott0f  38341  n0el2  38507  dfrel5  38518  dfrel6  38519  redundeq1  38885  dmqscoelseq  38918  dfeldisj5  38985  atbase  39586  llnbase  39806  lplnbase  39831  lvolbase  39875  lhpbase  40295  cdlemg31b0N  40991  cdlemg31b0a  40992  cdlemh  41114  sticksstones16  42453  sticksstones21  42458  unitscyglem3  42488  onsupmaxb  43517  iunrelexp0  43979  frege120  44260  clsk1indlem4  44321  gneispace  44411  scotteld  44523  undisjrab  44583  zfregs2VD  45117  dvnprod  46229  fnresfnco  47323  aiotavb  47372  afvpcfv0  47428  aovpcov0  47472  aov0ov0  47475  aovov0bi  47478  fnotaovb  47480  funressndmafv2rn  47505  fmtnoprmfac1lem  47846  lighneallem2  47888  stgrvtx0  48244  isubgr3stgrlem6  48253  pgnbgreunbgrlem2lem1  48396  pgnbgreunbgrlem2lem2  48397  pgnbgreunbgrlem2lem3  48398  snlindsntor  48753  rrx2pnedifcoorneorr  48999  itschlc0xyqsol1  49048  2itscp  49063  resinsn  49153  resinsnALT  49154  opndisj  49184  istermc  49755  lanrcl  49902  ranrcl  49903