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

Theorem eqeq2i 2811
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 2810 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538
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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791
This theorem is referenced by:  eqeq12i  2813  eqtri  2821  neeq2i  3052  rabid2  3334  rabid2f  3335  dfss2OLD  3902  equncom  4081  absn  4543  rabrsn  4620  ssunpr  4725  sspr  4726  sstp  4727  preq12b  4741  preqsnd  4749  preq12nebg  4753  opthprneg  4755  opeqpr  5360  propssopi  5363  wefrc  5513  dfrel4v  6014  dfrel4  6015  orddif  6252  funopg  6358  funimaexg  6410  funcocnv2  6614  dffn5f  6711  fnressn  6897  fressnfv  6899  fnprb  6948  fntpb  6949  riotaeqimp  7119  fnov  7261  ovmpos  7277  onuninsuci  7535  fvresex  7643  elxp6  7705  el2xptp  7717  el2xptp0  7718  opiota  7739  tpossym  7907  qsid  8346  mapsncnv  8440  ixpsnf1o  8485  card1  9381  pm54.43lem  9413  cf0  9662  sdom2en01  9713  cardeq0  9963  enqbreq2  10331  addcompr  10432  mulcompr  10434  axrrecex  10574  negeq0  10929  muleqadd  11273  crne0  11618  dfnn3  11639  xmulneg1  12650  hasheq0  13720  hashbc  13807  hashf1lem2  13810  hash2pwpr  13830  eqwrds3  14316  cjne0  14514  sqrt00  14615  sqrtmsq2i  14739  cbvsum  15044  fsump1i  15116  cbvprod  15261  bpoly2  15403  bpoly3  15404  bpoly4  15405  absefib  15543  efieq1re  15544  xpccatid  17430  sgrpidmnd  17908  smndex2dnrinv  18072  isnsg4  18311  selvval  20790  mat1dimelbas  21076  pmatcollpw3fi1lem1  21391  2ndcctbss  22060  ptcnp  22227  ovolgelb  24084  ioorinv  24180  rolle  24593  plymul0or  24877  reeff1o  25042  sineq0  25116  coseq1  25117  1cubr  25428  atandm2  25463  atandm3  25464  efrlim  25555  isppw  25699  ppiub  25788  lgsdinn0  25929  m1lgs  25972  uhgr2edg  26998  usgredg2vlem1  27015  usgredg2vlem2  27016  ushgredgedg  27019  ushgredgedgloop  27021  edgnbusgreu  27157  nb3grprlem2  27171  nb3gr2nb  27174  usgredgsscusgredg  27249  usgr2wlkneq  27545  usgr2pthlem  27552  crctcshwlkn0  27607  wwlksn0s  27647  umgr2adedgwlk  27731  umgr2adedgspth  27734  elwwlks2s3  27737  elwwlks2ons3im  27740  rusgrnumwwlkl1  27754  clwlkclwwlkflem  27789  isfrgr  28045  frgr3v  28060  frgrregorufr0  28109  isgrpo  28280  vciOLD  28344  chnlei  29268  h1de2ctlem  29338  cmcmlem  29374  cmcm2i  29376  cmbr2i  29379  osumcor2i  29427  pjss2i  29463  ho01i  29611  nmop0h  29774  pjclem1  29978  jplem1  30051  atabs2i  30185  fedgmullem2  31114  ccfldextdgrr  31145  zarcls  31227  breprexp  32014  bnj168  32110  bnj927  32150  bnj543  32275  bnj970  32329  subfacp1lem6  32545  satfv1  32723  satfvsucsuc  32725  satf0  32732  fmlaomn0  32750  fmla0disjsuc  32758  satffunlem2lem1  32764  mppspstlem  32931  quad3  33026  trpredmintr  33183  brdomain  33507  brrange  33508  brimg  33511  brapply  33512  brsuccf  33515  brfullfun  33522  brrestrict  33523  rankeq1o  33745  bj-snsetex  34399  bj-reabeq  34463  bj-rest10  34503  bj-ismooredr2  34525  bj-pinftynminfty  34642  dffinxpf  34802  finxp0  34808  matunitlindflem1  35053  ismblfin  35098  opropabco  35162  fdc  35183  isdrngo1  35394  smprngopr  35490  cdleme25cv  37654  cdlemk35  38208  dicval2  38475  dicopelval2  38477  dicelval2N  38478  hdmap1fval  39092  sn-0tie0  39574  mzpcompact2lem  39690  eldioph4b  39750  2nn0ind  39884  islmodfg  40011  relintab  40281  brtrclfv2  40426  frege116  40678  elnev  41140  dvnprodlem1  42586  fourierdlem103  42849  fourierdlem104  42850  ovnovollem3  43295  fmtno4prmfac  44087  lindsrng01  44875  ldepspr  44880  nn0sumshdiglemB  45032
  Copyright terms: Public domain W3C validator