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

Theorem syl5eleqr 2549
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 2462 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2548 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    e. wcel 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449
This theorem is referenced by:  rabsnt  4093  reusv6OLD  4648  onnev  5072  opabiota  5911  canth  6229  onnseq  7007  tfrlem16  7054  oen0  7227  nnawordex  7278  inf0  8029  cantnflt  8082  cantnfltOLD  8112  cnfcom2  8137  cnfcom3lem  8138  cnfcom3  8139  cnfcom2OLD  8145  cnfcom3lemOLD  8146  cnfcom3OLD  8147  r1ordg  8187  r1val1  8195  rankr1id  8271  acacni  8511  dfacacn  8512  dfac13  8513  cda1dif  8547  ttukeylem5  8884  ttukeylem6  8885  gch2  9042  gch3  9043  gchac  9048  gchina  9066  swrds1  12667  sadcp1  14189  xpsfrnel2  15054  idfucl  15369  gsumval2  16106  gsumz  16204  frmdmnd  16226  frmd0  16227  efginvrel2  16944  efgcpbl2  16974  pgpfaclem1  17327  lbsexg  18005  frlmlbs  18999  mat0dimscm  19138  mat0scmat  19207  m2detleiblem5  19294  m2detleiblem6  19295  m2detleiblem3  19298  m2detleiblem4  19299  d0mat2pmat  19406  chpmat0d  19502  dfac14  20285  acufl  20584  cnextfvval  20731  cnextcn  20733  minveclem3b  22009  minveclem4a  22011  ovollb2  22066  ovolunlem1a  22073  ovolunlem1  22074  ovoliunlem1  22079  ovoliun2  22083  ioombl1lem4  22137  uniioombllem1  22156  uniioombllem2  22158  uniioombllem6  22163  itg2monolem1  22323  itg2mono  22326  itg2cnlem1  22334  xrlimcnp  23496  efrlim  23497  eengbas  24486  ebtwntg  24487  ecgrtg  24488  elntg  24489  cusgrares  24674  usgrcyclnl1  24842  ex-br  25354  vcoprne  25670  rge0scvg  28166  mrsub0  29140  elmrsubrn  29144  topjoin  30423  aomclem1  31239  dfac21  31251  fourierdlem102  32230  fourierdlem114  32242  lincval0  33270  lcoel0  33283  pclfinN  36021
  Copyright terms: Public domain W3C validator