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

Theorem eqeq2i 2663
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 2662 . 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  eqtri  2673  neeq2i  2888  rabid2  3148  rabid2f  3149  dfss2  3624  equncom  3791  rabrsn  4291  ssunpr  4397  sspr  4398  sstp  4399  preq12b  4413  preqsnd  4423  preqsn  4424  preqsnOLD  4425  opeqpr  4997  propssopi  5000  wefrc  5137  dfrel4v  5619  dfrel4  5620  orddif  5858  dfiota2  5890  funopg  5960  funimaexg  6013  funcocnv2  6199  dffn5f  6291  fnressn  6465  fressnfv  6467  fnprb  6513  fntpb  6514  riotaeqimp  6674  fnov  6810  ovmpt2s  6826  onuninsuci  7082  fvresex  7181  elxp6  7244  el2xptp  7255  el2xptp0  7256  opiota  7273  tpossym  7429  qsid  7856  mapsncnv  7946  ixpsnf1o  7990  card1  8832  pm54.43lem  8863  cf0  9111  sdom2en01  9162  cardeq0  9412  enqbreq2  9780  addcompr  9881  mulcompr  9883  axrrecex  10022  negeq0  10373  muleqadd  10709  crne0  11051  dfnn3  11072  xmulneg1  12137  hasheq0  13192  hashbc  13275  hashf1lem2  13278  hash2pwpr  13296  eqwrds3  13750  cjne0  13947  sqrt00  14048  sqrtmsq2i  14171  cbvsum  14469  fsump1i  14544  cbvprod  14689  bpoly2  14832  bpoly3  14833  bpoly4  14834  absefib  14972  efieq1re  14973  xpccatid  16875  isnsg4  17684  mat1dimelbas  20325  pmatcollpw3fi1lem1  20639  2ndcctbss  21306  ptcnp  21473  ovolgelb  23294  ioorinv  23390  rolle  23798  plymul0or  24081  reeff1o  24246  sineq0  24318  coseq1  24319  1cubr  24614  atandm2  24649  atandm3  24650  efrlim  24741  isppw  24885  ppiub  24974  lgsdinn0  25115  m1lgs  25158  uhgr2edg  26145  usgredg2vlem1  26162  usgredg2vlem2  26163  ushgredgedg  26166  ushgredgedgloop  26168  edgnbusgreu  26313  nb3grprlem2  26327  nb3gr2nb  26330  usgredgsscusgredg  26411  usgr2wlkneq  26708  usgr2pthlem  26715  crctcshwlkn0  26769  wwlksn0s  26815  umgr2adedgwlk  26910  umgr2adedgspth  26913  elwwlks2s3  26916  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  rusgrnumwwlkl1  26935  frgr3v  27255  frgrregorufr0  27304  isgrpo  27479  vciOLD  27544  chnlei  28472  h1de2ctlem  28542  cmcmlem  28578  cmcm2i  28580  cmbr2i  28583  osumcor2i  28631  pjss2i  28667  ho01i  28815  nmop0h  28978  pjclem1  29182  jplem1  29255  atabs2i  29389  breprexp  30839  bnj168  30924  bnj927  30965  bnj543  31089  bnj970  31143  subfacp1lem6  31293  mppspstlem  31594  quad3  31690  trpredmintr  31855  brdomain  32165  brrange  32166  brimg  32169  brapply  32170  brsuccf  32173  brfullfun  32180  brrestrict  32181  rankeq1o  32403  bj-snsetex  33076  bj-rest10  33166  bj-pinftynminfty  33244  dffinxpf  33352  finxp0  33358  matunitlindflem1  33535  ismblfin  33580  opropabco  33648  fdc  33671  isdrngo1  33885  smprngopr  33981  cdleme25cv  35963  cdlemk35  36517  dicval2  36785  dicopelval2  36787  dicelval2N  36788  hdmap1fval  37403  mzpcompact2lem  37631  eldioph4b  37692  2nn0ind  37827  islmodfg  37956  relintab  38206  brtrclfv2  38336  frege116  38590  elnev  38956  dvnprodlem1  40479  fourierdlem103  40744  fourierdlem104  40745  ovnovollem3  41193  fmtno4prmfac  41809  lindsrng01  42582  ldepspr  42587  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator