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

Theorem syl6eqelr 2709
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl6eqelr.1 (𝜑𝐵 = 𝐴)
syl6eqelr.2 𝐵𝐶
Assertion
Ref Expression
syl6eqelr (𝜑𝐴𝐶)

Proof of Theorem syl6eqelr
StepHypRef Expression
1 syl6eqelr.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2627 . 2 (𝜑𝐴 = 𝐵)
3 syl6eqelr.2 . 2 𝐵𝐶
42, 3syl6eqel 2708 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1482  wcel 1989
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704  df-cleq 2614  df-clel 2617
This theorem is referenced by:  wemoiso2  7151  releldm2  7215  mapprc  7858  ixpprc  7926  bren  7961  brdomg  7962  ctex  7967  domssex  8118  mapen  8121  ssenen  8131  fodomfib  8237  fi0  8323  dffi3  8334  brwdom  8469  brwdomn0  8471  unxpwdom2  8490  ixpiunwdom  8493  tcmin  8614  rankonid  8689  rankr1id  8722  cardf2  8766  cardid2  8776  carduni  8804  fseqen  8847  acndom  8871  acndom2  8874  alephnbtwn  8891  cardcf  9071  cfeq0  9075  cflim2  9082  coftr  9092  infpssr  9127  hsmexlem5  9249  axdc3lem4  9272  fodomb  9345  ondomon  9382  gruina  9637  ioof  12268  hashbc  13232  hashfacen  13233  trclun  13749  zsum  14443  fsum  14445  fsumcom2OLD  14500  fprod  14665  fprodcom2OLD  14709  xpsfrnel2  16219  eqgen  17641  symgbas  17794  symgfisg  17882  dvdsr  18640  asplss  19323  aspsubrg  19325  psrval  19356  clsf  20846  restco  20962  subbascn  21052  is2ndc  21243  ptbasin2  21375  ptbas  21376  indishmph  21595  ufldom  21760  cnextfres1  21866  ussid  22058  icopnfcld  22565  cnrehmeo  22746  csscld  23042  clsocv  23043  itg2gt0  23521  dvmptadd  23717  dvmptmul  23718  dvmptco  23729  logcn  24387  selberglem1  25228  hmopidmchi  28994  sigagensiga  30189  dya2iocbrsiga  30322  dya2icobrsiga  30323  logdivsqrle  30713  fnessref  32336  unirep  33487  indexdom  33509  dicfnN  36298  pwslnmlem0  37487  mendval  37579  icof  39233  dvsubf  39897  dvdivf  39906  itgsinexplem1  39938  stirlinglem7  40066  fourierdlem73  40165  fouriersw  40217  ovolval4lem1  40632
  Copyright terms: Public domain W3C validator