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

Theorem syl5eleqr 2562
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 2475 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2561 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  rabsnt  4104  reusv6OLD  4658  onnev  5082  opabiota  5928  canth  6240  onnseq  7012  tfrlem16  7059  oen0  7232  nnawordex  7283  inf0  8034  cantnflt  8087  cantnfltOLD  8117  cnfcom2  8142  cnfcom3lem  8143  cnfcom3  8144  cnfcom2OLD  8150  cnfcom3lemOLD  8151  cnfcom3OLD  8152  r1ordg  8192  r1val1  8200  rankr1id  8276  acacni  8516  dfacacn  8517  dfac13  8518  cda1dif  8552  ttukeylem5  8889  ttukeylem6  8890  gch2  9049  gch3  9050  gchac  9055  gchina  9073  swrds1  12635  sadcp1  13960  xpsfrnel2  14816  idfucl  15104  gsumz  15824  gsumval2  15826  frmdmnd  15850  frmd0  15851  efginvrel2  16541  efgcpbl2  16571  pgpfaclem1  16922  lbsexg  17593  frlmlbs  18598  mat0dimscm  18738  mat0scmat  18807  m2detleiblem5  18894  m2detleiblem6  18895  m2detleiblem3  18898  m2detleiblem4  18899  d0mat2pmat  19006  chpmat0d  19102  dfac14  19854  acufl  20153  cnextfvval  20300  cnextcn  20302  minveclem3b  21578  minveclem4a  21580  ovollb2  21635  ovolunlem1a  21642  ovolunlem1  21643  ovoliunlem1  21648  ovoliun2  21652  ioombl1lem4  21706  uniioombllem1  21725  uniioombllem2  21727  uniioombllem6  21732  itg2monolem1  21892  itg2mono  21895  itg2cnlem1  21903  xrlimcnp  23026  efrlim  23027  eengbas  23960  ebtwntg  23961  ecgrtg  23962  elntg  23963  cusgrares  24148  usgrcyclnl1  24316  ex-br  24829  vcoprne  25148  rge0scvg  27567  topjoin  29786  aomclem1  30604  dfac21  30616  lincval0  32089  lcoel0  32102  pclfinN  34696
  Copyright terms: Public domain W3C validator