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 205   = wceq 1539

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728

This theorem is referenced by:  eqeq12i  2754  neeq1i  3006  ssequn2  4123  ineqcom  4142  sseqin2  4155  dfss7  4180  dfss4  4198  rabeq0w  4323  rabeq0  4324  disj  4387  disjOLD  4388  disjr  4389  undisj1  4401  undisj2  4402  undif  4421  uneqdifeq  4429  rabeqsn  4606  reusn  4667  rabsneu  4669  eusn  4670  tppreqb  4744  elpreqpr  4803  uniintsn  4925  iin0  5293  dfepfr  5585  epfrc  5586  dmopab3  5841  dm0rn0  5846  ssdmres  5926  iresn0n0  5973  imadisj  5998  args  6010  dffr3  6017  intirr  6038  dminxp  6098  dfrel3  6116  coeq0  6173  sspred  6226  dffr4  6237  frpomin2  6259  frpoind  6260  tz6.26OLD  6266  wfiOLD  6269  cbviotavw  6418  fntpg  6523  fncnv  6536  mptfnf  6598  sbcfng  6627  f0rn0  6689  dff1o4  6754  dffv4  6801  tz6.12c  6826  fvun2  6892  fnreseql  6957  funopdmsn  7054  f1ofvswap  7210  riota1  7286  riota2df  7288  riotaeqimp  7291  fnbrovb  7356  ovid  7446  ov  7449  ovg  7469  ovima0  7483  opiota  7931  frrlem13  8145  wfrlem8OLD  8178  tz7.49c  8308  sucprcreg  9404  zfregfr  9407  inf3lem2  9431  zfregs2  9535  frind  9552  rankxpsuc  9684  scott0s  9690  cplem1  9691  cfslb2n  10070  fin23lem26  10127  dfacfin7  10201  axdc3lem4  10255  zorn2lem7  10304  alephom  10387  fpwwe2  10445  recmulnq  10766  recexsr  10909  map2psrpr  10912  renegcli  11328  addeq0  11444  elznn0  12380  xrsupss  13089  xrinfmss  13090  prinfzo0  13472  seqf1olem1  13808  seqf1olem2  13809  sqeqori  13976  hashrabsn1  14134  hashprb  14157  hashprdifel  14158  hashbclem  14209  hash2pwpr  14235  f1oun2prg  14675  modfsummods  15550  cshwrepswhash1  16849  ismgmid  18394  smndex2dnrinv  18599  oppgid  19008  lsmdisjr  19335  gexex  19499  gsumxp2  19626  dprd0  19679  oppr1  19921  opprunit  19948  opprdomn  20617  zringndrg  20735  gsummoncoe1  21520  mat0dimcrng  21664  iinopn  22096  elcls  22269  ordthaus  22580  hauscmplem  22602  regr1lem2  22936  metdseq0  24062  minveclem1  24633  minveclem3b  24637  volun  24754  dyaddisj  24805  vieta1  25517  logeftb  25784  birthdaylem1  26146  dmgmaddn0  26217  gausslemma2d  26567  lgseisenlem1  26568  2lgslem4  26599  rpvmasum  26719  axsegconlem6  27335  edg0iedg0  27470  numedglnl  27559  ushgredgedg  27641  ushgredgedgloop  27643  uhgr0v0e  27650  usgr1v0edg  27669  usgrexmpllem  27672  usgr1v0e  27738  nbuhgr2vtx1edgblem  27763  uvtx01vtx  27809  prcliscplgr  27826  cusgr0v  27840  vtxdg0e  27886  1loopgrvd2  27915  finsumvtxdg2ssteplem4  27960  finsumvtxdg2size  27962  isrgr  27971  fusgrregdegfi  27981  wspn0  28334  2wlkdlem8  28343  3wlkdlem8  28576  uhgr3cyclexlem  28590  1to2vfriswmgr  28688  1to3vfriswmgr  28689  frgrregorufr0  28733  frgrreg  28803  frgrregord013  28804  ex-ceil  28857  nmlno0lem  29200  minvecolem1  29281  hvsubeq0i  29470  hvsubaddi  29473  pjoc2i  29845  pjoml3i  29993  cmbr3i  30007  pjss2i  30087  hosubeq0i  30233  dmadjrnb  30313  nmlnop0iALT  30402  nmopcoadj0i  30510  stm1ri  30651  jplem2  30676  atoml2i  30790  chirredlem1  30797  cdj3lem3  30845  difininv  30909  undifr  30917  disjnf  30954  disjpreima  30968  disjunsn  30978  f1od2  31101  wrdt2ind  31270  lsmsnorb2  31625  zrhchr  31971  ddemeas  32249  braew  32255  aean  32257  eulerpartlemgh  32390  ballotlemfp1  32503  repr0  32636  hgt750lem2  32677  bnj1143  32815  nummin  33108  acycgr0v  33155  prclisacycgr  33158  cvmsss2  33281  cvmlift2lem13  33322  snres0  33720  elrn3  33774  sltsolem1  33923  noinfbnd2lem1  33978  madeval2  34082  made0  34102  rankeq1o  34518  hfun  34525  bj-disj2r  35262  bj-sscon  35263  bj-0int  35316  bj-imdirco  35405  bj-pinftynminfty  35442  finxpreclem4  35609  nlpineqsn  35623  curunc  35803  tan2h  35813  poimirlem13  35834  poimirlem14  35835  poimirlem21  35842  poimirlem22  35843  asindmre  35904  totbndbnd  35991  rngosn3  36126  scott0f  36371  n0el2  36510  dfrel5  36523  dfrel6  36524  redundeq1  36784  dmqscoelseq  36815  dfeldisj5  36874  atbase  37345  llnbase  37565  lplnbase  37590  lvolbase  37634  lhpbase  38054  cdlemg31b0N  38750  cdlemg31b0a  38751  cdlemh  38873  sticksstones16  40160  sticksstones21  40165  metakunt24  40190  iunrelexp0  41348  frege120  41629  clsk1indlem4  41692  gneispace  41782  scotteld  41902  undisjrab  41962  zfregs2VD  42499  dvnprod  43539  fnresfnco  44593  aiotavb  44640  afvpcfv0  44696  aovpcov0  44740  aov0ov0  44743  aovov0bi  44746  fnotaovb  44748  funressndmafv2rn  44773  fmtnoprmfac1lem  45074  lighneallem2  45116  snlindsntor  45870  rrx2pnedifcoorneorr  46121  itschlc0xyqsol1  46170  2itscp  46185  opndisj  46254