MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeq1i Structured version   Visualization version   GIF version

Theorem eqeq1i 2656
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
StepHypRef Expression
1 eqeq1i.1 . 2 𝐴 = 𝐵
2 eqeq1 2655 . 2 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
31, 2ax-mp 5 1 (𝐴 = 𝐶𝐵 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  eqeq12i  2665  neeq1i  2887  ssequn2  3819  sseqin2  3850  dfss1OLD  3851  dfss4  3891  rabeq0  3990  disj  4050  disjr  4051  undisj1  4062  undisj2  4063  undif  4082  uneqdifeq  4090  uneqdifeqOLD  4091  reusn  4294  rabsneu  4296  eusn  4297  tppreqb  4368  elpreqpr  4427  uniintsn  4546  iin0  4869  opeqsn  4996  dfepfr  5128  epfrc  5129  dmopab3  5369  dm0rn0  5374  ssdmres  5455  imadisj  5519  args  5528  dffr3  5533  intirr  5549  dminxp  5609  dfrel3  5627  coeq0  5682  sspred  5726  dffr4  5734  tz6.26  5749  wfi  5751  unisuc  5839  fntpg  5986  fncnv  6000  mptfnf  6053  sbcfng  6080  f0rn0  6128  dff1o4  6183  dffv4  6226  fvun2  6309  fnreseql  6367  funopdmsn  6455  riota1  6669  riota2df  6671  riotaeqimp  6674  fnbrovb  6734  fnotovbOLD  6736  ovid  6819  ov  6822  ovg  6841  ovima0  6855  opiota  7273  wfrlem8  7467  tz7.49c  7586  sucprcreg  8544  zfregfr  8547  inf3lem2  8564  zfregs2  8647  rankxpsuc  8783  scott0s  8789  cplem1  8790  cfslb2n  9128  fin23lem26  9185  dfacfin7  9259  axdc3lem4  9313  zorn2lem7  9362  alephom  9445  fpwwe2  9503  recmulnq  9824  recexsr  9966  map2psrpr  9969  renegcli  10380  elznn0  11430  xrsupss  12177  xrinfmss  12178  prinfzo0  12546  seqf1olem1  12880  seqf1olem2  12881  sqeqori  13016  hashrabsn1  13201  hashprb  13223  hashprdifel  13224  hashbclem  13274  hash2pwpr  13296  swrdccat3a  13540  f1oun2prg  13708  modfsummods  14569  cshwrepswhash1  15856  ismgmid  17311  oppgid  17832  lsmdisjr  18143  gexex  18302  dprd0  18476  oppr1  18680  opprunit  18707  opprdomn  19349  gsummoncoe1  19722  zringndrg  19886  mat0dimcrng  20324  iinopn  20755  elcls  20925  ordthaus  21236  hauscmplem  21257  regr1lem2  21591  metdseq0  22704  minveclem1  23241  minveclem3b  23245  volun  23359  dyaddisj  23410  vieta1  24112  logeftb  24375  birthdaylem1  24723  dmgmaddn0  24794  gausslemma2d  25144  lgseisenlem1  25145  2lgslem4  25176  rpvmasum  25260  axsegconlem6  25847  edg0iedg0  25994  numedglnl  26084  ushgredgedg  26166  ushgredgedgloop  26168  uhgr0v0e  26175  usgr1v0edg  26194  usgrexmpllem  26197  usgr1v0e  26263  nbuhgr2vtx1edgblem  26292  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  prcliscplgr  26365  cusgr0v  26380  vtxdg0e  26426  1loopgrvd2  26455  finsumvtxdg2ssteplem4  26500  finsumvtxdg2size  26502  isrgr  26511  fusgrregdegfi  26521  wlknwwlksnsur  26844  wlkwwlksur  26851  wspn0  26889  2wlkdlem8  26898  clwlksfclwwlk1hashn  27046  clwlksfoclwwlk  27050  3wlkdlem8  27145  uhgr3cyclexlem  27159  1to2vfriswmgr  27259  1to3vfriswmgr  27260  frgrregorufr0  27304  frgrreg  27381  frgrregord013  27382  ex-ceil  27435  nmlno0lem  27776  minvecolem1  27858  hvsubeq0i  28048  hvsubaddi  28051  pjoc2i  28425  pjoml3i  28573  cmbr3i  28587  pjss2i  28667  hosubeq0i  28813  dmadjrnb  28893  nmlnop0iALT  28982  nmopcoadj0i  29090  stm1ri  29231  jplem2  29256  atoml2i  29370  chirredlem1  29377  cdj3lem3  29425  difininv  29480  disjnf  29510  disjpreima  29523  disjunsn  29533  f1od2  29627  addeq0  29638  zrhchr  30148  ddemeas  30427  braew  30433  aean  30435  eulerpartlemgh  30568  ballotlemfp1  30681  repr0  30817  hgt750lem2  30858  bnj1143  30987  cvmsss2  31382  cvmlift2lem13  31423  elrn3  31778  frpomin2  31864  frpoind  31865  frind  31868  sltsolem1  31951  madeval2  32061  rankeq1o  32403  hfun  32410  bj-disj2r  33138  bj-sscon  33139  bj-0int  33180  bj-pinftynminfty  33244  finxpreclem4  33361  curunc  33521  tan2h  33531  poimirlem13  33552  poimirlem14  33553  poimirlem21  33560  poimirlem22  33561  asindmre  33625  totbndbnd  33718  rngosn3  33853  scott0f  34107  ineqcom  34148  n0el2  34244  dfrel5  34254  dfrel6  34255  atbase  34894  llnbase  35113  lplnbase  35138  lvolbase  35182  lhpbase  35602  cdlemg31b0N  36299  cdlemg31b0a  36300  cdlemh  36422  iunrelexp0  38311  frege120  38594  clsk1indlem4  38659  gneispace  38749  undisjrab  38822  zfregs2VD  39390  dvnprod  40482  fnresfnco  41527  afvpcfv0  41547  aovpcov0  41591  aov0ov0  41594  aovov0bi  41597  fnotaovb  41599  fmtnoprmfac1lem  41801  lighneallem2  41848  snlindsntor  42585
  Copyright terms: Public domain W3C validator