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

Theorem syl5sseqr 3552
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseqr.1
syl5sseqr.2
Assertion
Ref Expression
syl5sseqr

Proof of Theorem syl5sseqr
StepHypRef Expression
1 syl5sseqr.1 . . 3
21a1i 11 . 2
3 syl5sseqr.2 . 2
42, 3sseqtr4d 3540 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  unissint  4311  resdif  5841  fimacnv  6019  tfrlem5  7068  domss2  7696  dffi3  7911  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  trcl  8180  tcid  8191  r1ordg  8217  r1sssuc  8222  ackbij1lem15  8635  cfsmolem  8671  isfin4-3  8716  fin1a2lem7  8807  wunex2  9137  wuncid  9142  fsumsplit  13562  o1fsum  13627  fprodsplit  13770  phimullem  14309  vdwlem6  14504  ressinbas  14693  mrcssid  15014  mreexexlem2d  15042  acsfiindd  15807  dirge  15867  symgbasfi  16411  efgredlemf  16759  efgredlemd  16762  gsumzres  16914  gsumzcl2  16915  gsumzf1o  16917  gsumzresOLD  16918  gsumzclOLD  16919  gsumzf1oOLD  16920  gsumzaddlemOLD  16936  gsumadd  16938  gsumaddOLD  16939  gsumzsplit  16944  gsumzsplitOLD  16945  gsumsplit2  16948  gsumsplit2OLD  16949  gsumzoppgOLD  16968  dprd2da  17091  dmdprdsplit2lem  17094  dmdprdsplit2  17095  dmdprdsplit  17096  dprdsplit  17097  invrpropd  17347  issubdrg  17454  lspssid  17631  aspssid  17982  pjcss  18747  istopon  19426  sscls  19557  ordtbas  19693  cncls2  19774  tgcmp  19901  cmpfi  19908  1stcfb  19946  1stckgenlem  20054  ptbasfi  20082  ptcnplem  20122  ptuncnv  20308  ptunhmeo  20309  fbasrn  20385  cnflf2  20504  fclscmp  20531  alexsublem  20544  ghmcnp  20613  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmssplit  20654  tsmsxplem1  20655  ustssco  20717  mopnfss  20946  cnmpt2pc  21428  uniiccdif  21987  uniioombllem3  21994  uniioombllem4  21995  itg2splitlem  22155  itg2split  22156  itgsplit  22242  ellimc2  22281  ellimc3  22283  lhop  22417  plyaddlem1  22610  plymullem1  22611  taylthlem2  22769  mtest  22799  xrlimcnp  23298  fsumharmonic  23341  chtdif  23432  dchrghm  23531  lgsquadlem2  23630  dchrisumlema  23673  dchrisumlem2  23675  dchrisum0lem1b  23700  dchrisum0lem1  23701  pntrlog2bndlem6  23768  pntlemf  23790  ex-res  25162  spanss2  26263  mdsymi  27330  ordtconlem1  27906  issgon  28123  sssigagen  28145  measiuns  28188  sitgclg  28284  cvmliftlem10  28739  rtrclreclem.refl  29067  ftc1anclem6  30095  heibor1lem  30305  heibor  30317  divrngcl  30360  isdrngo2  30361  igenss  30459  nacsfix  30644  isnumbasgrplem2  31053  rgspnssid  31119  itgpowd  31182  icccncfext  31690  iblsplit  31765  dirkeritg  31884  dirkercncflem2  31886  fourierdlem81  31970  fourierdlem89  31978  fourierdlem91  31980  fourierdlem92  31981  fourierdlem111  32000  fouriercn  32015  srhmsubc  32884  srhmsubcOLD  32903  gsumsplit2f  32954  paddunssN  35532  sspadd1  35539  sspadd2  35540  pclssidN  35619  diassdvaN  36787  dochvalr  37084  lcdvbase  37320  wnefimgd  37974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator