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

Theorem eqeq2i 2783
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 2782 . 2 (𝐴 = 𝐵 → (𝐶 = 𝐴𝐶 = 𝐵))
31, 2ax-mp 5 1 (𝐶 = 𝐴𝐶 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1631
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  eqeq12i  2785  eqtri  2793  neeq2i  3008  rabid2  3267  rabid2f  3268  dfss2  3740  equncom  3909  rabrsn  4395  ssunpr  4498  sspr  4499  sstp  4500  preq12b  4513  preqsnd  4523  preqsndOLD  4524  preqsnOLD  4528  preq12nebg  4529  opthprneg  4531  opeqpr  5097  propssopi  5101  wefrc  5243  dfrel4v  5725  dfrel4  5726  orddif  5963  dfiota2  5995  funopg  6065  funimaexg  6115  funcocnv2  6302  dffn5f  6394  fnressn  6568  fressnfv  6570  fnprb  6616  fntpb  6617  riotaeqimp  6777  fnov  6915  ovmpt2s  6931  onuninsuci  7187  fvresex  7286  elxp6  7349  el2xptp  7360  el2xptp0  7361  opiota  7378  tpossym  7536  qsid  7965  mapsncnv  8058  ixpsnf1o  8102  card1  8994  pm54.43lem  9025  cf0  9275  sdom2en01  9326  cardeq0  9576  enqbreq2  9944  addcompr  10045  mulcompr  10047  axrrecex  10186  negeq0  10537  muleqadd  10873  crne0  11215  dfnn3  11236  xmulneg1  12304  hasheq0  13356  hashbc  13439  hashf1lem2  13442  hash2pwpr  13460  eqwrds3  13914  cjne0  14111  sqrt00  14212  sqrtmsq2i  14335  cbvsum  14633  fsump1i  14708  cbvprod  14852  bpoly2  14994  bpoly3  14995  bpoly4  14996  absefib  15134  efieq1re  15135  xpccatid  17036  isnsg4  17845  mat1dimelbas  20495  pmatcollpw3fi1lem1  20811  2ndcctbss  21479  ptcnp  21646  ovolgelb  23468  ioorinv  23564  rolle  23973  plymul0or  24256  reeff1o  24421  sineq0  24494  coseq1  24495  1cubr  24790  atandm2  24825  atandm3  24826  efrlim  24917  isppw  25061  ppiub  25150  lgsdinn0  25291  m1lgs  25334  uhgr2edg  26322  usgredg2vlem1  26339  usgredg2vlem2  26340  ushgredgedg  26343  ushgredgedgloop  26345  ushgredgedgloopOLD  26346  edgnbusgreu  26491  edgnbusgreuOLD  26492  nb3grprlem2  26506  nb3gr2nb  26509  usgredgsscusgredg  26590  usgr2wlkneq  26887  usgr2pthlem  26894  crctcshwlkn0  26949  wwlksn0s  26995  umgr2adedgwlk  27092  umgr2adedgspth  27095  elwwlks2s3  27098  elwwlks2ons3im  27101  elwwlks2ons3OLD  27103  rusgrnumwwlkl1  27117  clwlkclwwlkflem  27154  frgr3v  27457  frgrregorufr0  27506  isgrpo  27691  vciOLD  27756  chnlei  28684  h1de2ctlem  28754  cmcmlem  28790  cmcm2i  28792  cmbr2i  28795  osumcor2i  28843  pjss2i  28879  ho01i  29027  nmop0h  29190  pjclem1  29394  jplem1  29467  atabs2i  29601  breprexp  31051  bnj168  31136  bnj927  31177  bnj543  31301  bnj970  31355  subfacp1lem6  31505  mppspstlem  31806  quad3  31902  trpredmintr  32067  brdomain  32377  brrange  32378  brimg  32381  brapply  32382  brsuccf  32385  brfullfun  32392  brrestrict  32393  rankeq1o  32615  bj-snsetex  33282  bj-rest10  33373  bj-pinftynminfty  33451  dffinxpf  33559  finxp0  33565  matunitlindflem1  33738  ismblfin  33783  opropabco  33850  fdc  33873  isdrngo1  34087  smprngopr  34183  cdleme25cv  36167  cdlemk35  36721  dicval2  36989  dicopelval2  36991  dicelval2N  36992  hdmap1fval  37606  mzpcompact2lem  37840  eldioph4b  37901  2nn0ind  38036  islmodfg  38165  relintab  38415  brtrclfv2  38545  frege116  38799  elnev  39165  dvnprodlem1  40679  fourierdlem103  40943  fourierdlem104  40944  ovnovollem3  41392  fmtno4prmfac  42012  lindsrng01  42785  ldepspr  42790  nn0sumshdiglemB  42942
  Copyright terms: Public domain W3C validator