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

Theorem eqeq2i 2834
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 2833 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  eqeq12i  2836  eqtri  2844  neeq2i  3081  rabid2  3382  rabid2f  3383  dfss2  3954  equncom  4129  absn  4577  rabrsn  4654  ssunpr  4759  sspr  4760  sstp  4761  preq12b  4775  preqsnd  4783  preq12nebg  4787  opthprneg  4789  opeqpr  5387  propssopi  5390  wefrc  5543  dfrel4v  6041  dfrel4  6042  orddif  6278  funopg  6383  funimaexg  6434  funcocnv2  6633  dffn5f  6730  fnressn  6913  fressnfv  6915  fnprb  6963  fntpb  6964  riotaeqimp  7129  fnov  7271  ovmpos  7287  onuninsuci  7543  fvresex  7652  elxp6  7714  el2xptp  7726  el2xptp0  7727  opiota  7748  tpossym  7915  qsid  8353  mapsncnv  8446  ixpsnf1o  8491  card1  9386  pm54.43lem  9417  cf0  9662  sdom2en01  9713  cardeq0  9963  enqbreq2  10331  addcompr  10432  mulcompr  10434  axrrecex  10574  negeq0  10929  muleqadd  11273  crne0  11620  dfnn3  11641  xmulneg1  12652  hasheq0  13714  hashbc  13801  hashf1lem2  13804  hash2pwpr  13824  eqwrds3  14315  cjne0  14512  sqrt00  14613  sqrtmsq2i  14737  cbvsum  15042  fsump1i  15114  cbvprod  15259  bpoly2  15401  bpoly3  15402  bpoly4  15403  absefib  15541  efieq1re  15542  xpccatid  17428  sgrpidmnd  17906  isnsg4  18259  selvval  20261  mat1dimelbas  21010  pmatcollpw3fi1lem1  21324  2ndcctbss  21993  ptcnp  22160  ovolgelb  24010  ioorinv  24106  rolle  24516  plymul0or  24799  reeff1o  24964  sineq0  25038  coseq1  25039  1cubr  25347  atandm2  25382  atandm3  25383  efrlim  25475  isppw  25619  ppiub  25708  lgsdinn0  25849  m1lgs  25892  uhgr2edg  26918  usgredg2vlem1  26935  usgredg2vlem2  26936  ushgredgedg  26939  ushgredgedgloop  26941  edgnbusgreu  27077  nb3grprlem2  27091  nb3gr2nb  27094  usgredgsscusgredg  27169  usgr2wlkneq  27465  usgr2pthlem  27472  crctcshwlkn0  27527  wwlksn0s  27567  umgr2adedgwlk  27652  umgr2adedgspth  27655  elwwlks2s3  27658  elwwlks2ons3im  27661  rusgrnumwwlkl1  27675  clwlkclwwlkflem  27710  isfrgr  27967  frgr3v  27982  frgrregorufr0  28031  isgrpo  28202  vciOLD  28266  chnlei  29190  h1de2ctlem  29260  cmcmlem  29296  cmcm2i  29298  cmbr2i  29301  osumcor2i  29349  pjss2i  29385  ho01i  29533  nmop0h  29696  pjclem1  29900  jplem1  29973  atabs2i  30107  fedgmullem2  30926  ccfldextdgrr  30957  breprexp  31804  bnj168  31900  bnj927  31940  bnj543  32065  bnj970  32119  subfacp1lem6  32330  satfv1  32508  satfvsucsuc  32510  satf0  32517  fmlaomn0  32535  fmla0disjsuc  32543  satffunlem2lem1  32549  mppspstlem  32716  quad3  32811  trpredmintr  32968  brdomain  33292  brrange  33293  brimg  33296  brapply  33297  brsuccf  33300  brfullfun  33307  brrestrict  33308  rankeq1o  33530  bj-snsetex  34173  bj-reabeq  34237  bj-rest10  34274  bj-ismooredr2  34297  bj-pinftynminfty  34402  dffinxpf  34549  finxp0  34555  matunitlindflem1  34770  ismblfin  34815  opropabco  34882  fdc  34903  isdrngo1  35117  smprngopr  35213  cdleme25cv  37376  cdlemk35  37930  dicval2  38197  dicopelval2  38199  dicelval2N  38200  hdmap1fval  38814  mzpcompact2lem  39228  eldioph4b  39288  2nn0ind  39422  islmodfg  39549  relintab  39823  brtrclfv2  39952  frege116  40205  elnev  40650  dvnprodlem1  42111  fourierdlem103  42375  fourierdlem104  42376  ovnovollem3  42821  fmtno4prmfac  43581  smndex2dnrinv  43985  lindsrng01  44421  ldepspr  44426  nn0sumshdiglemB  44578
  Copyright terms: Public domain W3C validator