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

Theorem syl5eleqr 2520
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 2438 . 2  |-  ( ph  ->  B  =  C )
41, 3syl5eleq 2519 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429
This theorem is referenced by:  rabsnt  3940  reusv6OLD  4491  onnev  4908  opabiota  5742  canth  6036  onnseq  6791  tfrlem16  6838  oen0  7013  nnawordex  7064  inf0  7815  cantnflt  7868  cantnfltOLD  7898  cnfcom2  7923  cnfcom3lem  7924  cnfcom3  7925  cnfcom2OLD  7931  cnfcom3lemOLD  7932  cnfcom3OLD  7933  r1ordg  7973  r1val1  7981  rankr1id  8057  acacni  8297  dfacacn  8298  dfac13  8299  cda1dif  8333  ttukeylem5  8670  ttukeylem6  8671  gch2  8829  gch3  8830  gchac  8835  gchina  8853  swrds1  12328  sadcp1  13633  xpsfrnel2  14485  idfucl  14773  gsumz  15490  gsumval2  15492  frmdmnd  15516  frmd0  15517  efginvrel2  16203  efgcpbl2  16233  pgpfaclem1  16555  lbsexg  17166  frlmlbs  18066  m2detleiblem5  18272  m2detleiblem6  18273  m2detleiblem3  18276  m2detleiblem4  18277  dfac14  19032  acufl  19331  cnextfvval  19478  cnextcn  19480  minveclem3b  20756  minveclem4a  20758  ovollb2  20813  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliun2  20830  ioombl1lem4  20883  uniioombllem1  20902  uniioombllem2  20904  uniioombllem6  20909  itg2monolem1  21069  itg2mono  21072  itg2cnlem1  21080  xrlimcnp  22246  efrlim  22247  eengbas  23049  ebtwntg  23050  ecgrtg  23051  elntg  23052  cusgrares  23202  usgrcyclnl1  23348  ex-br  23460  vcoprne  23779  rge0scvg  26232  topjoin  28427  aomclem1  29249  dfac21  29261  mat0dimscm  30642  lincval0  30655  lcoel0  30668  pclfinN  33114
  Copyright terms: Public domain W3C validator