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 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2446  df-clel 2449
This theorem is referenced by:  rabsnt  4059  reusv6OLD  4610  onnev  5028  opabiota  5862  canth  6157  onnseq  6914  tfrlem16  6961  oen0  7134  nnawordex  7185  inf0  7937  cantnflt  7990  cantnfltOLD  8020  cnfcom2  8045  cnfcom3lem  8046  cnfcom3  8047  cnfcom2OLD  8053  cnfcom3lemOLD  8054  cnfcom3OLD  8055  r1ordg  8095  r1val1  8103  rankr1id  8179  acacni  8419  dfacacn  8420  dfac13  8421  cda1dif  8455  ttukeylem5  8792  ttukeylem6  8793  gch2  8952  gch3  8953  gchac  8958  gchina  8976  swrds1  12462  sadcp1  13768  xpsfrnel2  14621  idfucl  14909  gsumz  15629  gsumval2  15631  frmdmnd  15655  frmd0  15656  efginvrel2  16344  efgcpbl2  16374  pgpfaclem1  16703  lbsexg  17367  frlmlbs  18349  m2detleiblem5  18562  m2detleiblem6  18563  m2detleiblem3  18566  m2detleiblem4  18567  dfac14  19322  acufl  19621  cnextfvval  19768  cnextcn  19770  minveclem3b  21046  minveclem4a  21048  ovollb2  21103  ovolunlem1a  21110  ovolunlem1  21111  ovoliunlem1  21116  ovoliun2  21120  ioombl1lem4  21174  uniioombllem1  21193  uniioombllem2  21195  uniioombllem6  21200  itg2monolem1  21360  itg2mono  21363  itg2cnlem1  21371  xrlimcnp  22494  efrlim  22495  eengbas  23378  ebtwntg  23379  ecgrtg  23380  elntg  23381  cusgrares  23531  usgrcyclnl1  23677  ex-br  23789  vcoprne  24108  rge0scvg  26523  topjoin  28733  aomclem1  29554  dfac21  29566  mat0dimscm  31030  lincval0  31067  lcoel0  31080  d0mat2pmat  31213  cpmat0d  31305  pclfinN  33867
  Copyright terms: Public domain W3C validator