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

Theorem syl5sseqr 3389
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 3377 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312
This theorem is referenced by:  unissint  4066  resdif  5688  fimacnv  5854  domss2  7258  dffi3  7428  cantnfp1lem3  7628  trcl  7656  tcid  7670  r1ordg  7696  r1sssuc  7701  ackbij1lem15  8106  cfsmolem  8142  isfin4-3  8187  fin1a2lem7  8278  wunex2  8605  wuncid  8610  fsumsplit  12525  o1fsum  12584  phimullem  13160  vdwlem6  13346  ressinbas  13517  mrcssid  13834  mreexexlem2d  13862  acsfiindd  14595  dirge  14674  efgredlemf  15365  efgredlemd  15368  gsumzres  15509  gsumzcl  15510  gsumzf1o  15511  gsumzaddlem  15518  gsumadd  15520  gsumzsplit  15521  gsumsplit2  15523  gsumconst  15524  gsumzoppg  15531  dprd2da  15592  dmdprdsplit2lem  15595  dmdprdsplit2  15596  dmdprdsplit  15597  dprdsplit  15598  invrpropd  15795  issubdrg  15885  lspssid  16053  aspssid  16384  pjcss  16935  istopon  16982  sscls  17112  ordtbas  17248  cncls2  17329  tgcmp  17456  cmpfi  17463  1stcfb  17500  1stckgenlem  17577  ptbasfi  17605  ptcnplem  17645  ptuncnv  17831  ptunhmeo  17832  fbasrn  17908  cnflf2  18027  fclscmp  18054  alexsublem  18067  ghmcnp  18136  tsmsgsum  18160  tsmsres  18165  tsmssplit  18173  tsmsxplem1  18174  ustssco  18236  mopnfss  18465  cnmpt2pc  18945  uniiccdif  19462  uniioombllem3  19469  uniioombllem4  19470  itg2splitlem  19632  itg2split  19633  itgsplit  19719  ellimc2  19756  ellimc3  19758  lhop  19892  plyaddlem1  20124  plymullem1  20125  taylthlem2  20282  mtest  20312  xrlimcnp  20799  fsumharmonic  20842  chtdif  20933  dchrghm  21032  lgsquadlem2  21131  dchrisumlema  21174  dchrisumlem2  21176  dchrisum0lem1b  21201  dchrisum0lem1  21202  pntrlog2bndlem6  21269  pntlemf  21291  ex-res  21741  spanss2  22839  mdsymi  23906  issgon  24498  sssigagen  24520  measiuns  24563  cvmliftlem10  24973  rtrclreclem.refl  25136  fprodsplit  25281  ftc1anclem6  26275  heibor1lem  26509  heibor  26521  divrngcl  26564  isdrngo2  26565  igenss  26663  nacsfix  26757  isnumbasgrplem2  27237  rgspnssid  27343  paddunssN  30542  sspadd1  30549  sspadd2  30550  pclssidN  30629  diassdvaN  31795  dochvalr  32092  lcdvbase  32328
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator