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

Theorem syl5sseqr 3553
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 3541 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    C_ wss 3476
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-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  unissint  4306  resdif  5836  fimacnv  6013  tfrlem5  7049  domss2  7676  dffi3  7891  cantnfp1lem3  8099  cantnfp1lem3OLD  8125  trcl  8159  tcid  8170  r1ordg  8196  r1sssuc  8201  ackbij1lem15  8614  cfsmolem  8650  isfin4-3  8695  fin1a2lem7  8786  wunex2  9116  wuncid  9121  fsumsplit  13525  o1fsum  13590  phimullem  14168  vdwlem6  14363  ressinbas  14551  mrcssid  14872  mreexexlem2d  14900  acsfiindd  15664  dirge  15724  symgbasfi  16216  efgredlemf  16565  efgredlemd  16568  gsumzres  16717  gsumzcl2  16718  gsumzf1o  16720  gsumzresOLD  16721  gsumzclOLD  16722  gsumzf1oOLD  16723  gsumzaddlemOLD  16739  gsumadd  16741  gsumaddOLD  16742  gsumzsplit  16747  gsumzsplitOLD  16748  gsumsplit2  16751  gsumsplit2OLD  16752  gsumzoppgOLD  16771  dprd2da  16893  dmdprdsplit2lem  16896  dmdprdsplit2  16897  dmdprdsplit  16898  dprdsplit  16899  invrpropd  17148  issubdrg  17254  lspssid  17431  aspssid  17781  pjcss  18542  istopon  19221  sscls  19351  ordtbas  19487  cncls2  19568  tgcmp  19695  cmpfi  19702  1stcfb  19740  1stckgenlem  19817  ptbasfi  19845  ptcnplem  19885  ptuncnv  20071  ptunhmeo  20072  fbasrn  20148  cnflf2  20267  fclscmp  20294  alexsublem  20307  ghmcnp  20376  tsmsgsum  20400  tsmsgsumOLD  20403  tsmsresOLD  20408  tsmsres  20409  tsmssplit  20417  tsmsxplem1  20418  ustssco  20480  mopnfss  20709  cnmpt2pc  21191  uniiccdif  21750  uniioombllem3  21757  uniioombllem4  21758  itg2splitlem  21918  itg2split  21919  itgsplit  22005  ellimc2  22044  ellimc3  22046  lhop  22180  plyaddlem1  22373  plymullem1  22374  taylthlem2  22531  mtest  22561  xrlimcnp  23054  fsumharmonic  23097  chtdif  23188  dchrghm  23287  lgsquadlem2  23386  dchrisumlema  23429  dchrisumlem2  23431  dchrisum0lem1b  23456  dchrisum0lem1  23457  pntrlog2bndlem6  23524  pntlemf  23546  ex-res  24867  spanss2  25967  mdsymi  27034  ordtconlem1  27570  issgon  27791  sssigagen  27813  measiuns  27856  sitgclg  27952  cvmliftlem10  28407  rtrclreclem.refl  28570  fprodsplit  28700  ftc1anclem6  29700  heibor1lem  29936  heibor  29948  divrngcl  29991  isdrngo2  29992  igenss  30090  nacsfix  30276  isnumbasgrplem2  30685  rgspnssid  30752  itgpowd  30815  icccncfext  31254  dirkeritg  31430  fourierdlem81  31516  fourierdlem92  31527  gsumsplit2f  32051  paddunssN  34622  sspadd1  34629  sspadd2  34630  pclssidN  34709  diassdvaN  35875  dochvalr  36172  lcdvbase  36408
  Copyright terms: Public domain W3C validator