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

Theorem eqeq2i 2831
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 2830 . 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 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  eqeq12i  2833  eqtri  2841  neeq2i  3078  rabid2  3379  rabid2f  3380  dfss2  3952  equncom  4127  absn  4575  rabrsn  4652  ssunpr  4757  sspr  4758  sstp  4759  preq12b  4773  preqsnd  4781  preq12nebg  4785  opthprneg  4787  opeqpr  5386  propssopi  5389  wefrc  5542  dfrel4v  6040  dfrel4  6041  orddif  6277  funopg  6382  funimaexg  6433  funcocnv2  6632  dffn5f  6729  fnressn  6912  fressnfv  6914  fnprb  6962  fntpb  6963  riotaeqimp  7129  fnov  7271  ovmpos  7287  onuninsuci  7544  fvresex  7650  elxp6  7712  el2xptp  7724  el2xptp0  7725  opiota  7746  tpossym  7913  qsid  8352  mapsncnv  8445  ixpsnf1o  8490  card1  9385  pm54.43lem  9416  cf0  9661  sdom2en01  9712  cardeq0  9962  enqbreq2  10330  addcompr  10431  mulcompr  10433  axrrecex  10573  negeq0  10928  muleqadd  11272  crne0  11619  dfnn3  11640  xmulneg1  12650  hasheq0  13712  hashbc  13799  hashf1lem2  13802  hash2pwpr  13822  eqwrds3  14313  cjne0  14510  sqrt00  14611  sqrtmsq2i  14735  cbvsum  15040  fsump1i  15112  cbvprod  15257  bpoly2  15399  bpoly3  15400  bpoly4  15401  absefib  15539  efieq1re  15540  xpccatid  17426  sgrpidmnd  17904  isnsg4  18257  selvval  20259  mat1dimelbas  21008  pmatcollpw3fi1lem1  21322  2ndcctbss  21991  ptcnp  22158  ovolgelb  24008  ioorinv  24104  rolle  24514  plymul0or  24797  reeff1o  24962  sineq0  25036  coseq1  25037  1cubr  25347  atandm2  25382  atandm3  25383  efrlim  25474  isppw  25618  ppiub  25707  lgsdinn0  25848  m1lgs  25891  uhgr2edg  26917  usgredg2vlem1  26934  usgredg2vlem2  26935  ushgredgedg  26938  ushgredgedgloop  26940  edgnbusgreu  27076  nb3grprlem2  27090  nb3gr2nb  27093  usgredgsscusgredg  27168  usgr2wlkneq  27464  usgr2pthlem  27471  crctcshwlkn0  27526  wwlksn0s  27566  umgr2adedgwlk  27651  umgr2adedgspth  27654  elwwlks2s3  27657  elwwlks2ons3im  27660  rusgrnumwwlkl1  27674  clwlkclwwlkflem  27709  isfrgr  27966  frgr3v  27981  frgrregorufr0  28030  isgrpo  28201  vciOLD  28265  chnlei  29189  h1de2ctlem  29259  cmcmlem  29295  cmcm2i  29297  cmbr2i  29300  osumcor2i  29348  pjss2i  29384  ho01i  29532  nmop0h  29695  pjclem1  29899  jplem1  29972  atabs2i  30106  fedgmullem2  30925  ccfldextdgrr  30956  breprexp  31803  bnj168  31899  bnj927  31939  bnj543  32064  bnj970  32118  subfacp1lem6  32329  satfv1  32507  satfvsucsuc  32509  satf0  32516  fmlaomn0  32534  fmla0disjsuc  32542  satffunlem2lem1  32548  mppspstlem  32715  quad3  32810  trpredmintr  32967  brdomain  33291  brrange  33292  brimg  33295  brapply  33296  brsuccf  33299  brfullfun  33306  brrestrict  33307  rankeq1o  33529  bj-snsetex  34172  bj-reabeq  34236  bj-rest10  34273  bj-ismooredr2  34296  bj-pinftynminfty  34401  dffinxpf  34548  finxp0  34554  matunitlindflem1  34769  ismblfin  34814  opropabco  34880  fdc  34901  isdrngo1  35115  smprngopr  35211  cdleme25cv  37374  cdlemk35  37928  dicval2  38195  dicopelval2  38197  dicelval2N  38198  hdmap1fval  38812  mzpcompact2lem  39226  eldioph4b  39286  2nn0ind  39420  islmodfg  39547  relintab  39821  brtrclfv2  39950  frege116  40203  elnev  40647  dvnprodlem1  42107  fourierdlem103  42371  fourierdlem104  42372  ovnovollem3  42817  fmtno4prmfac  43611  smndex2dnrinv  44015  lindsrng01  44451  ldepspr  44456  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator