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

Theorem eqeq2i 2749
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 2748 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2728
This theorem is referenced by:  eqeq12i  2754  eqtri  2764  neeq2i  3007  rabid2f  3433  rabid2OLD  3435  abv  3454  dfss2OLD  3929  equncom  4112  eq0  4301  ab0w  4331  ab0  4332  ab0OLD  4333  ab0orv  4336  eq0rdv  4362  rzal  4464  absn  4602  rabrsn  4683  ssunpr  4790  sspr  4791  sstp  4792  preq12b  4806  preqsnd  4814  preq12nebg  4818  opthprneg  4820  opeqpr  5460  propssopi  5463  wefrc  5625  dfrel4v  6140  dfrel4  6141  orddif  6411  funopg  6532  funimaexgOLD  6585  funcocnv2  6806  dffn5f  6910  fnressn  7100  fressnfv  7102  fnprb  7154  fntpb  7155  riotaeqimp  7336  fnov  7483  ovmpos  7499  onuninsuci  7772  fvresex  7888  elxp6  7951  el2xptp  7963  el2xptp0  7964  opiota  7987  tpossym  8185  dfwrecsOLD  8240  qsid  8718  mapsncnv  8827  ixpsnf1o  8872  card1  9900  pm54.43lem  9932  cf0  10183  sdom2en01  10234  cardeq0  10484  enqbreq2  10852  addcompr  10953  mulcompr  10955  axrrecex  11095  negeq0  11451  muleqadd  11795  crne0  12142  dfnn3  12163  xmulneg1  13180  hasheq0  14255  hashbc  14342  hashf1lem2  14347  hash2pwpr  14367  eqwrds3  14842  cjne0  15040  sqrt00  15140  sqrtmsq2i  15264  cbvsum  15572  fsump1i  15646  cbvprod  15790  bpoly2  15932  bpoly3  15933  bpoly4  15934  absefib  16072  efieq1re  16073  xpccatid  18068  sgrpidmnd  18553  smndex2dnrinv  18717  isnsg4  18960  selvval  21512  mat1dimelbas  21804  pmatcollpw3fi1lem1  22119  2ndcctbss  22790  ptcnp  22957  ovolgelb  24828  ioorinv  24924  rolle  25338  plymul0or  25625  reeff1o  25790  sineq0  25864  coseq1  25865  1cubr  26176  atandm2  26211  atandm3  26212  efrlim  26303  isppw  26447  ppiub  26536  lgsdinn0  26677  m1lgs  26720  uhgr2edg  28042  usgredg2vlem1  28059  usgredg2vlem2  28060  ushgredgedg  28063  ushgredgedgloop  28065  edgnbusgreu  28201  nb3grprlem2  28215  nb3gr2nb  28218  usgredgsscusgredg  28293  usgr2wlkneq  28590  usgr2pthlem  28597  crctcshwlkn0  28652  wwlksn0s  28692  umgr2adedgwlk  28776  umgr2adedgspth  28779  elwwlks2s3  28782  elwwlks2ons3im  28785  rusgrnumwwlkl1  28799  clwlkclwwlkflem  28834  isfrgr  29090  frgr3v  29105  frgrregorufr0  29154  isgrpo  29325  vciOLD  29389  chnlei  30313  h1de2ctlem  30383  cmcmlem  30419  cmcm2i  30421  cmbr2i  30424  osumcor2i  30472  pjss2i  30508  ho01i  30656  nmop0h  30819  pjclem1  31023  jplem1  31096  atabs2i  31230  fedgmullem2  32202  ccfldextdgrr  32233  zarcls  32324  breprexp  33115  bnj168  33211  bnj927  33250  bnj543  33374  bnj970  33428  subfacp1lem6  33648  satfv1  33826  satfvsucsuc  33828  satf0  33835  fmlaomn0  33853  fmla0disjsuc  33861  satffunlem2lem1  33867  mppspstlem  34034  quad3  34127  brdomain  34485  brrange  34486  brimg  34489  brapply  34490  brsuccf  34493  brfullfun  34500  brrestrict  34501  rankeq1o  34723  bj-snsetex  35401  bj-reabeq  35465  bj-rest10  35526  bj-ismooredr2  35548  bj-pinftynminfty  35665  dffinxpf  35823  finxp0  35829  matunitlindflem1  36041  ismblfin  36086  opropabco  36150  fdc  36171  isdrngo1  36382  smprngopr  36478  eldisjlem19  37239  cdleme25cv  38788  cdlemk35  39342  dicval2  39609  dicopelval2  39611  dicelval2N  39612  hdmap1fval  40226  sn-0tie0  40846  mzpcompact2lem  41012  eldioph4b  41072  2nn0ind  41207  islmodfg  41334  abeqabi  41622  relintab  41797  brtrclfv2  41941  frege116  42193  elnev  42660  dvnprodlem1  44119  fourierdlem103  44382  fourierdlem104  44383  ovnovollem3  44831  fmtno4prmfac  45696  lindsrng01  46481  ldepspr  46486  nn0sumshdiglemB  46638  mofeu  46846
  Copyright terms: Public domain W3C validator