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

Theorem eqeq2i 2632
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 2631 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613
This theorem is referenced by:  eqeq12i  2634  eqtri  2642  neeq2i  2856  rabid2  3113  rabid2f  3114  dfss2  3584  equncom  3750  rabrsn  4250  ssunpr  4356  sspr  4357  sstp  4358  preq12b  4373  preqsnd  4383  preqsn  4384  preqsnOLD  4385  opeqpr  4958  propssopi  4961  wefrc  5098  dfrel4v  5572  dfrel4  5573  orddif  5808  dfiota2  5840  funopg  5910  funimaexg  5963  funcocnv2  6148  dffn5f  6239  fnressn  6410  fressnfv  6412  fnprb  6457  fntpb  6458  riotaeqimp  6619  fnov  6753  ovmpt2s  6769  onuninsuci  7025  fvresex  7124  elxp6  7185  el2xptp  7196  el2xptp0  7197  opiota  7214  tpossym  7369  qsid  7798  mapsncnv  7889  ixpsnf1o  7933  card1  8779  pm54.43lem  8810  cf0  9058  sdom2en01  9109  cardeq0  9359  enqbreq2  9727  addcompr  9828  mulcompr  9830  axrrecex  9969  negeq0  10320  muleqadd  10656  crne0  10998  dfnn3  11019  xmulneg1  12084  hasheq0  13137  hashbc  13220  hashf1lem2  13223  hash2pwpr  13241  eqwrds3  13685  cjne0  13884  sqrt00  13985  sqrtmsq2i  14108  cbvsum  14406  fsump1i  14481  cbvprod  14626  bpoly2  14769  bpoly3  14770  bpoly4  14771  absefib  14909  efieq1re  14910  xpccatid  16809  isnsg4  17618  mat1dimelbas  20258  pmatcollpw3fi1lem1  20572  2ndcctbss  21239  ptcnp  21406  ovolgelb  23229  ioorinv  23325  rolle  23734  plymul0or  24017  reeff1o  24182  sineq0  24254  coseq1  24255  1cubr  24550  atandm2  24585  atandm3  24586  efrlim  24677  isppw  24821  ppiub  24910  lgsdinn0  25051  m1lgs  25094  uhgr2edg  26081  usgredg2vlem1  26098  usgredg2vlem2  26099  ushgredgedg  26102  ushgredgedgloop  26104  edgnbusgreu  26250  nb3grprlem2  26264  nb3gr2nb  26267  usgredgsscusgredg  26336  usgr2wlkneq  26633  usgr2pthlem  26640  crctcshwlkn0  26694  wwlksn0s  26727  umgr2adedgwlk  26822  umgr2adedgspth  26825  elwwlks2ons3  26829  elwwlks2s3  26840  rusgrnumwwlkl1  26844  frgr3v  27119  frgrregorufr0  27162  isgrpo  27321  vciOLD  27386  chnlei  28314  h1de2ctlem  28384  cmcmlem  28420  cmcm2i  28422  cmbr2i  28425  osumcor2i  28473  pjss2i  28509  ho01i  28657  nmop0h  28820  pjclem1  29024  jplem1  29097  atabs2i  29231  breprexp  30685  bnj168  30772  bnj927  30813  bnj543  30937  bnj970  30991  subfacp1lem6  31141  mppspstlem  31442  quad3  31538  trpredmintr  31705  brdomain  32015  brrange  32016  brimg  32019  brapply  32020  brsuccf  32023  brfullfun  32030  brrestrict  32031  rankeq1o  32253  bj-snsetex  32926  bj-rest10  33016  bj-pinftynminfty  33085  dffinxpf  33193  finxp0  33199  matunitlindflem1  33376  ismblfin  33421  opropabco  33489  fdc  33512  isdrngo1  33726  smprngopr  33822  cdleme25cv  35465  cdlemk35  36019  dicval2  36287  dicopelval2  36289  dicelval2N  36290  hdmap1fval  36905  mzpcompact2lem  37133  eldioph4b  37194  2nn0ind  37329  islmodfg  37458  relintab  37708  brtrclfv2  37838  frege116  38093  elnev  38459  dvnprodlem1  39924  fourierdlem103  40189  fourierdlem104  40190  ovnovollem3  40635  fmtno4prmfac  41249  lindsrng01  42022  ldepspr  42027  nn0sumshdiglemB  42179
  Copyright terms: Public domain W3C validator