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

Theorem syl5sseqr 3513
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseqr.1  |-  B  C_  A
syl5sseqr.2  |-  ( ph  ->  C  =  A )
Assertion
Ref Expression
syl5sseqr  |-  ( ph  ->  B  C_  C )

Proof of Theorem syl5sseqr
StepHypRef Expression
1 syl5sseqr.1 . . 3  |-  B  C_  A
21a1i 11 . 2  |-  ( ph  ->  B  C_  A )
3 syl5sseqr.2 . 2  |-  ( ph  ->  C  =  A )
42, 3sseqtr4d 3501 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  unissint  4280  resdif  5851  fimacnv  6027  tfrlem5  7109  domss2  7740  dffi3  7954  cantnfp1lem3  8193  trcl  8220  tcid  8231  r1ordg  8257  r1sssuc  8262  ackbij1lem15  8671  cfsmolem  8707  isfin4-3  8752  fin1a2lem7  8843  wunex2  9170  wuncid  9175  trclfvlb  13072  rtrclreclem1  13121  fsumsplit  13805  o1fsum  13872  fprodsplit  14019  phimullem  14726  vdwlem6  14935  ressinbas  15184  mrcssid  15522  mreexexlem2d  15550  acsfiindd  16422  dirge  16482  symgbasfi  17026  efgredlemf  17390  efgredlemd  17393  gsumzres  17542  gsumzcl2  17543  gsumzf1o  17545  gsumadd  17555  gsumzsplit  17559  gsumsplit2  17561  dprd2da  17674  dmdprdsplit2lem  17677  dmdprdsplit2  17678  dmdprdsplit  17679  dprdsplit  17680  invrpropd  17925  issubdrg  18032  lspssid  18207  aspssid  18556  pjcss  19277  istopon  19938  sscls  20069  ordtbas  20206  cncls2  20287  tgcmp  20414  cmpfi  20421  1stcfb  20458  1stckgenlem  20566  ptbasfi  20594  ptcnplem  20634  ptuncnv  20820  ptunhmeo  20821  fbasrn  20897  cnflf2  21016  fclscmp  21043  alexsublem  21057  ghmcnp  21127  tsmsgsum  21151  tsmsres  21156  tsmssplit  21164  tsmsxplem1  21165  ustssco  21227  mopnfss  21456  cnmpt2pc  21954  uniiccdif  22533  uniioombllem3  22541  uniioombllem4  22542  itg2splitlem  22704  itg2split  22705  itgsplit  22791  ellimc2  22830  ellimc3  22832  lhop  22966  plyaddlem1  23165  plymullem1  23166  taylthlem2  23327  mtest  23357  xrlimcnp  23892  fsumharmonic  23935  chtdif  24083  dchrghm  24182  lgsquadlem2  24281  dchrisumlema  24324  dchrisumlem2  24326  dchrisum0lem1b  24351  dchrisum0lem1  24352  pntrlog2bndlem6  24419  pntlemf  24441  ex-res  25889  spanss2  26996  mdsymi  28062  padct  28313  ordtconlem1  28738  issgon  28953  sssigagen  28975  measiuns  29047  sitgclg  29183  cvmliftlem10  30025  ftc1anclem6  31986  heibor1lem  32105  heibor  32117  divrngcl  32160  isdrngo2  32161  igenss  32259  paddunssN  33342  sspadd1  33349  sspadd2  33350  pclssidN  33429  diassdvaN  34597  dochvalr  34894  lcdvbase  35130  nacsfix  35523  isnumbasgrplem2  35933  rgspnssid  36006  itgpowd  36069  trrelsuperrel2dg  36233  fvilbd  36251  relexp0a  36278  wnefimgd  36570  icccncfext  37705  iblsplit  37783  dirkeritg  37904  dirkercncflem2  37906  fourierdlem81  37991  fourierdlem89  37999  fourierdlem91  38001  fourierdlem92  38002  fourierdlem111  38021  fouriercn  38036  srhmsubc  39697  srhmsubcALTV  39716  gsumsplit2f  39767  fdivmpt  39972  fdivpm  39975  refdivpm  39976
  Copyright terms: Public domain W3C validator