MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5eleqr Structured version   Unicode version

Theorem syl5eleqr 2536
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eleqr.1  |-  A  e.  B
syl5eleqr.2  |-  ( ph  ->  C  =  B )
Assertion
Ref Expression
syl5eleqr  |-  ( ph  ->  A  e.  C )

Proof of Theorem syl5eleqr
StepHypRef Expression
1 syl5eleqr.1 . 2  |-  A  e.  B
2 syl5eleqr.2 . . 3  |-  ( ph  ->  C  =  B )
32eqcomd 2449 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2535 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1381    e. wcel 1802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-cleq 2433  df-clel 2436
This theorem is referenced by:  rabsnt  4088  reusv6OLD  4644  onnev  5070  opabiota  5917  canth  6235  onnseq  7013  tfrlem16  7060  oen0  7233  nnawordex  7284  inf0  8036  cantnflt  8089  cantnfltOLD  8119  cnfcom2  8144  cnfcom3lem  8145  cnfcom3  8146  cnfcom2OLD  8152  cnfcom3lemOLD  8153  cnfcom3OLD  8154  r1ordg  8194  r1val1  8202  rankr1id  8278  acacni  8518  dfacacn  8519  dfac13  8520  cda1dif  8554  ttukeylem5  8891  ttukeylem6  8892  gch2  9051  gch3  9052  gchac  9057  gchina  9075  swrds1  12650  sadcp1  13977  xpsfrnel2  14834  idfucl  15119  gsumval2  15776  gsumz  15874  frmdmnd  15896  frmd0  15897  efginvrel2  16614  efgcpbl2  16644  pgpfaclem1  17000  lbsexg  17678  frlmlbs  18698  mat0dimscm  18838  mat0scmat  18907  m2detleiblem5  18994  m2detleiblem6  18995  m2detleiblem3  18998  m2detleiblem4  18999  d0mat2pmat  19106  chpmat0d  19202  dfac14  19985  acufl  20284  cnextfvval  20431  cnextcn  20433  minveclem3b  21709  minveclem4a  21711  ovollb2  21766  ovolunlem1a  21773  ovolunlem1  21774  ovoliunlem1  21779  ovoliun2  21783  ioombl1lem4  21837  uniioombllem1  21856  uniioombllem2  21858  uniioombllem6  21863  itg2monolem1  22023  itg2mono  22026  itg2cnlem1  22034  xrlimcnp  23163  efrlim  23164  eengbas  24149  ebtwntg  24150  ecgrtg  24151  elntg  24152  cusgrares  24337  usgrcyclnl1  24505  ex-br  25017  vcoprne  25337  rge0scvg  27797  mrsub0  28742  elmrsubrn  28746  topjoin  30151  aomclem1  30968  dfac21  30980  fourierdlem102  31876  fourierdlem114  31888  lincval0  32726  lcoel0  32739  pclfinN  35326
  Copyright terms: Public domain W3C validator