Theorem eqeq1i 2826

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

Syntax hints:   ↔ wb 208   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  eqeq12i  2836  neeq1i  3080  ssequn2  4158  sseqin2  4191  dfss7  4216  dfss4  4234  rabeq0  4337  disj  4398  disjr  4399  undisj1  4410  undisj2  4411  undif  4429  uneqdifeq  4437  rabeqsn  4605  reusn  4662  rabsneu  4664  eusn  4665  tppreqb  4737  elpreqpr  4796  uniintsn  4912  iin0  5260  dfepfr  5539  epfrc  5540  dmopab3  5787  dm0rn0  5794  ssdmres  5875  iresn0n0  5922  imadisj  5947  args  5956  dffr3  5961  intirr  5977  dminxp  6036  dfrel3  6054  coeq0  6107  sspred  6155  dffr4  6163  tz6.26  6178  wfi  6180  unisuc  6266  fntpg  6413  fncnv  6426  mptfnf  6482  sbcfng  6510  f0rn0  6563  dff1o4  6622  dffv4  6666  fvun2  6754  fnreseql  6817  funopdmsn  6911  riota1  7134  riota2df  7136  riotaeqimp  7139  fnbrovb  7204  ovid  7290  ov  7293  ovg  7312  ovima0  7326  opiota  7756  wfrlem8  7961  tz7.49c  8081  sucprcreg  9064  zfregfr  9067  inf3lem2  9091  zfregs2  9174  rankxpsuc  9310  scott0s  9316  cplem1  9317  cfslb2n  9689  fin23lem26  9746  dfacfin7  9820  axdc3lem4  9874  zorn2lem7  9923  alephom  10006  fpwwe2  10064  recmulnq  10385  recexsr  10528  map2psrpr  10531  renegcli  10946  addeq0  11062  elznn0  11995  xrsupss  12701  xrinfmss  12702  prinfzo0  13075  seqf1olem1  13408  seqf1olem2  13409  sqeqori  13575  hashrabsn1  13734  hashprb  13757  hashprdifel  13758  hashbclem  13809  hash2pwpr  13833  f1oun2prg  14278  modfsummods  15147  cshwrepswhash1  16435  ismgmid  17874  smndex2dnrinv  18079  oppgid  18483  lsmdisjr  18809  gexex  18972  gsumxp2  19099  dprd0  19152  oppr1  19383  opprunit  19410  opprdomn  20073  gsummoncoe1  20471  zringndrg  20636  mat0dimcrng  21078  iinopn  21509  elcls  21680  ordthaus  21991  hauscmplem  22013  regr1lem2  22347  metdseq0  23461  minveclem1  24026  minveclem3b  24030  volun  24145  dyaddisj  24196  vieta1  24900  logeftb  25166  birthdaylem1  25528  dmgmaddn0  25599  gausslemma2d  25949  lgseisenlem1  25950  2lgslem4  25981  rpvmasum  26101  axsegconlem6  26707  edg0iedg0  26839  numedglnl  26928  ushgredgedg  27010  ushgredgedgloop  27012  uhgr0v0e  27019  usgr1v0edg  27038  usgrexmpllem  27041  usgr1v0e  27107  nbuhgr2vtx1edgblem  27132  uvtx01vtx  27178  prcliscplgr  27195  cusgr0v  27209  vtxdg0e  27255  1loopgrvd2  27284  finsumvtxdg2ssteplem4  27329  finsumvtxdg2size  27331  isrgr  27340  fusgrregdegfi  27350  wspn0  27702  2wlkdlem8  27711  3wlkdlem8  27945  uhgr3cyclexlem  27959  1to2vfriswmgr  28057  1to3vfriswmgr  28058  frgrregorufr0  28102  frgrreg  28172  frgrregord013  28173  ex-ceil  28226  nmlno0lem  28569  minvecolem1  28650  hvsubeq0i  28839  hvsubaddi  28842  pjoc2i  29214  pjoml3i  29362  cmbr3i  29376  pjss2i  29456  hosubeq0i  29602  dmadjrnb  29682  nmlnop0iALT  29771  nmopcoadj0i  29879  stm1ri  30020  jplem2  30045  atoml2i  30159  chirredlem1  30166  cdj3lem3  30214  difininv  30278  undifr  30283  disjnf  30319  disjpreima  30333  disjunsn  30343  f1od2  30456  wrdt2ind  30627  zrhchr  31217  ddemeas  31495  braew  31501  aean  31503  eulerpartlemgh  31636  ballotlemfp1  31749  repr0  31882  hgt750lem2  31923  bnj1143  32062  acycgr0v  32395  prclisacycgr  32398  cvmsss2  32521  cvmlift2lem13  32562  elrn3  32998  frpomin2  33079  frpoind  33080  frind  33085  frrlem13  33135  sltsolem1  33180  madeval2  33290  rankeq1o  33632  hfun  33639  bj-disj2r  34340  bj-sscon  34341  bj-0int  34392  bj-pinftynminfty  34508  finxpreclem4  34674  nlpineqsn  34688  curunc  34873  tan2h  34883  poimirlem13  34904  poimirlem14  34905  poimirlem21  34912  poimirlem22  34913  asindmre  34976  totbndbnd  35066  rngosn3  35201  scott0f  35446  ineqcom  35503  n0el2  35589  dfrel5  35602  dfrel6  35603  redundeq1  35863  dmqscoelseq  35894  dfeldisj5  35953  atbase  36424  llnbase  36644  lplnbase  36669  lvolbase  36713  lhpbase  37133  cdlemg31b0N  37829  cdlemg31b0a  37830  cdlemh  37952  iunrelexp0  40045  frege120  40327  clsk1indlem4  40392  gneispace  40482  scotteld  40580  undisjrab  40636  zfregs2VD  41173  dvnprod  42232  fnresfnco  43275  aiotavb  43289  afvpcfv0  43344  aovpcov0  43388  aov0ov0  43391  aovov0bi  43394  fnotaovb  43396  funressndmafv2rn  43421  fmtnoprmfac1lem  43725  lighneallem2  43770  snlindsntor  44525  rrx2pnedifcoorneorr  44703  itschlc0xyqsol1  44752  2itscp  44767