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

Theorem eqeq2i 2816
Description: Inference from equality to equivalence of equalities. (Contributed by NM, 26-May-1993.)
Hypothesis
Ref Expression
eqeq2i.1 𝐴 = 𝐵
Assertion
Ref Expression
eqeq2i (𝐶 = 𝐴𝐶 = 𝐵)

Proof of Theorem eqeq2i
StepHypRef Expression
1 eqeq2i.1 . 2 𝐴 = 𝐵
2 eqeq2 2815 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2782
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2797
This theorem is referenced by:  eqeq12i  2818  eqtri  2826  neeq2i  3041  rabid2  3305  rabid2f  3306  dfss2  3784  equncom  3955  absn  4386  rabrsn  4448  ssunpr  4551  sspr  4552  sstp  4553  preq12b  4567  preqsnd  4577  preqsndOLD  4578  preqsnOLD  4582  preq12nebg  4583  opthprneg  4585  opeqpr  5157  propssopi  5161  wefrc  5303  dfrel4v  5793  dfrel4  5794  orddif  6031  funopg  6133  funimaexg  6184  funcocnv2  6375  dffn5f  6471  fnressn  6647  fressnfv  6649  fnprb  6695  fntpb  6696  riotaeqimp  6856  fnov  6996  ovmpt2s  7012  onuninsuci  7268  fvresex  7367  elxp6  7430  el2xptp  7441  el2xptp0  7442  opiota  7459  tpossym  7617  qsid  8046  mapsncnv  8139  ixpsnf1o  8183  card1  9075  pm54.43lem  9106  cf0  9356  sdom2en01  9407  cardeq0  9657  enqbreq2  10025  addcompr  10126  mulcompr  10128  axrrecex  10267  negeq0  10618  muleqadd  10954  crne0  11296  dfnn3  11317  xmulneg1  12315  hasheq0  13370  hashbc  13452  hashf1lem2  13455  hash2pwpr  13473  eqwrds3  13927  cjne0  14124  sqrt00  14225  sqrtmsq2i  14348  cbvsum  14646  fsump1i  14721  cbvprod  14864  bpoly2  15006  bpoly3  15007  bpoly4  15008  absefib  15146  efieq1re  15147  xpccatid  17031  isnsg4  17837  mat1dimelbas  20486  pmatcollpw3fi1lem1  20802  2ndcctbss  21470  ptcnp  21637  ovolgelb  23459  ioorinv  23555  rolle  23965  plymul0or  24248  reeff1o  24413  sineq0  24486  coseq1  24487  1cubr  24781  atandm2  24816  atandm3  24817  efrlim  24908  isppw  25052  ppiub  25141  lgsdinn0  25282  m1lgs  25325  uhgr2edg  26313  usgredg2vlem1  26330  usgredg2vlem2  26331  ushgredgedg  26334  ushgredgedgloop  26336  ushgredgedgloopOLD  26337  edgnbusgreu  26482  edgnbusgreuOLD  26483  nb3grprlem2  26497  nb3gr2nb  26500  usgredgsscusgredg  26581  usgr2wlkneq  26878  usgr2pthlem  26885  crctcshwlkn0  26940  wwlksn0s  26986  umgr2adedgwlk  27083  umgr2adedgspth  27086  elwwlks2s3  27089  elwwlks2ons3im  27092  elwwlks2ons3OLD  27094  rusgrnumwwlkl1  27108  clwlkclwwlkflem  27145  frgr3v  27448  frgrregorufr0  27497  isgrpo  27678  vciOLD  27742  chnlei  28670  h1de2ctlem  28740  cmcmlem  28776  cmcm2i  28778  cmbr2i  28781  osumcor2i  28829  pjss2i  28865  ho01i  29013  nmop0h  29176  pjclem1  29380  jplem1  29453  atabs2i  29587  breprexp  31034  bnj168  31119  bnj927  31160  bnj543  31284  bnj970  31338  subfacp1lem6  31488  mppspstlem  31789  quad3  31884  trpredmintr  32049  brdomain  32359  brrange  32360  brimg  32363  brapply  32364  brsuccf  32367  brfullfun  32374  brrestrict  32375  rankeq1o  32597  bj-snsetex  33259  bj-rest10  33350  bj-pinftynminfty  33429  dffinxpf  33536  finxp0  33542  matunitlindflem1  33716  ismblfin  33761  opropabco  33828  fdc  33850  isdrngo1  34064  smprngopr  34160  cdleme25cv  36137  cdlemk35  36691  dicval2  36958  dicopelval2  36960  dicelval2N  36961  hdmap1fval  37575  mzpcompact2lem  37814  eldioph4b  37875  2nn0ind  38009  islmodfg  38138  relintab  38387  brtrclfv2  38517  frege116  38771  elnev  39136  dvnprodlem1  40639  fourierdlem103  40903  fourierdlem104  40904  ovnovollem3  41352  fmtno4prmfac  42057  lindsrng01  42823  ldepspr  42828  nn0sumshdiglemB  42980
  Copyright terms: Public domain W3C validator