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

Theorem syl5eleqr 2525
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 2443 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2524 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434
This theorem is referenced by:  rabsnt  3947  reusv6OLD  4498  onnev  4916  opabiota  5749  canth  6044  onnseq  6797  tfrlem16  6844  oen0  7017  nnawordex  7068  inf0  7819  cantnflt  7872  cantnfltOLD  7902  cnfcom2  7927  cnfcom3lem  7928  cnfcom3  7929  cnfcom2OLD  7935  cnfcom3lemOLD  7936  cnfcom3OLD  7937  r1ordg  7977  r1val1  7985  rankr1id  8061  acacni  8301  dfacacn  8302  dfac13  8303  cda1dif  8337  ttukeylem5  8674  ttukeylem6  8675  gch2  8834  gch3  8835  gchac  8840  gchina  8858  swrds1  12337  sadcp1  13643  xpsfrnel2  14495  idfucl  14783  gsumz  15502  gsumval2  15504  frmdmnd  15528  frmd0  15529  efginvrel2  16215  efgcpbl2  16245  pgpfaclem1  16572  lbsexg  17225  frlmlbs  18205  m2detleiblem5  18411  m2detleiblem6  18412  m2detleiblem3  18415  m2detleiblem4  18416  dfac14  19171  acufl  19470  cnextfvval  19617  cnextcn  19619  minveclem3b  20895  minveclem4a  20897  ovollb2  20952  ovolunlem1a  20959  ovolunlem1  20960  ovoliunlem1  20965  ovoliun2  20969  ioombl1lem4  21022  uniioombllem1  21041  uniioombllem2  21043  uniioombllem6  21048  itg2monolem1  21208  itg2mono  21211  itg2cnlem1  21219  xrlimcnp  22342  efrlim  22343  eengbas  23195  ebtwntg  23196  ecgrtg  23197  elntg  23198  cusgrares  23348  usgrcyclnl1  23494  ex-br  23606  vcoprne  23925  rge0scvg  26348  topjoin  28557  aomclem1  29378  dfac21  29390  mat0dimscm  30825  lincval0  30880  lcoel0  30893  pclfinN  33437
  Copyright terms: Public domain W3C validator