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

Theorem syl5ss 3190
Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
Hypotheses
Ref Expression
syl5ss.1  |-  A  C_  B
syl5ss.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5ss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5ss
StepHypRef Expression
1 syl5ss.1 . . 3  |-  A  C_  B
21a1i 10 . 2  |-  ( ph  ->  A  C_  B )
3 syl5ss.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3sstrd 3189 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3152
This theorem is referenced by:  wereu2  4390  sofld  5121  fvmptss  5609  fimacnv  5657  isofr2  5841  frxp  6225  fnse  6232  smores2  6371  ersym  6672  ertr  6675  f1imaen2g  6922  domunsncan  6962  fissuni  7160  fipreima  7161  finsschain  7162  dffi3  7184  marypha1lem  7186  ordtypelem7  7239  ordtypelem8  7240  oismo  7255  unxpwdom2  7302  oemapvali  7386  mapfien  7399  tskwe  7583  r0weon  7640  acndom2  7681  dfac2a  7756  dfac12lem2  7770  ackbij1lem16  7861  cfle  7880  cofsmo  7895  coftr  7899  fin23lem26  7951  fin23lem29  7967  isf32lem8  7986  isf34lem5  8004  isf34lem7  8005  isf34lem6  8006  enfin1ai  8010  fin1a2lem12  8037  ttukeylem7  8142  alephexp1  8201  fpwwe2lem13  8264  fpwwe2  8265  canth4  8269  canthwelem  8272  pwfseqlem1  8280  pwfseqlem4  8284  wunfi  8343  wunex2  8360  hashf1lem2  11394  limsupgle  11951  limsupgre  11955  rlimres  12032  lo1res  12033  lo1resb  12038  rlimresb  12039  o1resb  12040  o1of2  12086  o1rlimmul  12092  isercolllem2  12139  isercoll  12141  climsup  12143  sumsplit  12231  fsum2dlem  12233  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  bitsinvp1  12640  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  sadasslem  12661  sadeq  12663  bitsres  12664  smuval2  12673  smupval  12679  smueqlem  12681  smumul  12684  1arith  12974  isstruct2  13157  setscom  13176  ressress  13205  imasvscafn  13439  imasless  13442  mrcssv  13516  isacs1i  13559  mreacs  13560  acsfn  13561  yonedalem1  14046  yonedalem21  14047  yonedalem3a  14048  yonedalem4c  14051  yonedalem22  14052  yonedalem3b  14053  yonedainv  14055  yonffthlem  14056  isacs4lem  14271  isacs5lem  14272  mhmima  14440  cntzmhm  14814  efgval  15026  gsumzaddlem  15203  dmdprdd  15237  dprdfeq0  15257  dprdres  15263  dprdss  15264  dprdz  15265  subgdmdprd  15269  dprddisj2  15274  dprd2dlem1  15276  dprd2da  15277  dprd2d2  15279  dmdprdsplit2lem  15280  ablfac1eulem  15307  lmhmlsp  15806  lbspss  15835  lsmsp  15839  lspsolv  15896  lsppratlem3  15902  lsppratlem4  15903  lspprat  15906  islbs2  15907  islbs3  15908  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  mplcoe1  16209  mplcoe2  16211  mplind  16243  znleval  16508  basdif0  16691  tgcl  16707  ppttop  16744  epttop  16746  ntrin  16798  mretopd  16829  lpss3  16876  restlp  16913  ordtbas  16922  cnclsi  17001  cnconst2  17011  cnrest  17013  cnrest2  17014  cnpresti  17016  cnprest2  17018  lpcls  17092  fiuncmp  17131  connsub  17147  conima  17151  iunconlem  17153  1stcfb  17171  2ndc1stc  17177  2ndcdisj  17182  kgentopon  17233  llycmpkgen2  17245  1stckgenlem  17248  kgencn3  17253  ptclsg  17309  ptcnplem  17315  txtube  17334  hausdiag  17339  txkgen  17346  xkoco1cn  17351  xkoco2cn  17352  xkococnlem  17353  qtoptop2  17390  basqtop  17402  qtoprest  17408  imastopn  17411  hmeores  17462  hmphdis  17487  ptcmpfi  17504  fbssfi  17532  filin  17549  infil  17558  fbasrn  17579  fgtr  17585  isufil2  17603  ufileu  17614  filufint  17615  ufinffr  17624  elfm  17642  imaelfm  17646  fmfnfmlem4  17652  fmfnfm  17653  hausflim  17676  flimclslem  17679  fclsfnflim  17722  flimfnfcls  17723  fclscmp  17725  tmdgsum2  17779  cldsubg  17793  tgpconcomp  17795  tsmsres  17826  imasdsf1olem  17937  blin2  17975  icccmplem2  18328  icccmplem3  18329  reconnlem2  18332  xrge0gsumle  18338  fsumcn  18374  tchcph  18667  fmcfil  18698  bcthlem5  18750  resscdrg  18775  ivthlem2  18812  ivthlem3  18813  ivth2  18815  ovolfiniun  18860  ovoliunlem1  18861  ismbl2  18886  cmmbl  18892  nulmbl2  18894  unmbl  18895  shftmbl  18896  iundisj2  18906  voliunlem1  18907  voliunlem2  18908  ioombl1lem4  18918  uniiccdif  18933  uniioombllem4  18941  uniiccmbl  18945  dyadmbllem  18954  dyadmbl  18955  mbflimsup  19021  i1fima  19033  i1fima2  19034  itg1val2  19039  itg1cl  19040  itg1ge0  19041  i1fadd  19050  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  itg1mulc  19059  itg10a  19065  itg1ge0a  19066  itg1climres  19069  mbfi1fseqlem4  19073  itg2splitlem  19103  itg2split  19104  itgss3  19169  itgfsum  19181  limcdif  19226  limcnlp  19228  ellimc3  19229  limcflflem  19230  limcflf  19231  limcmpt2  19234  limcresi  19235  limciun  19244  perfdvf  19253  dvreslem  19259  dvres2lem  19260  dvres  19261  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvferm1  19332  dvferm2  19334  dvlip  19340  dvlip2  19342  c1liplem1  19343  dvivthlem1  19355  dvne0  19358  lhop1lem  19360  lhop  19363  dvcnvrelem1  19364  dvcnvrelem2  19365  dvfsumle  19368  dvfsumabs  19370  dvfsumlem2  19374  ftc1lem6  19388  itgsubstlem  19395  mdegleb  19450  mdeglt  19451  mdegldg  19452  mdegxrcl  19453  mdegcl  19455  ig1peu  19557  ig1pdvds  19562  taylthlem1  19752  taylthlem2  19753  ulmdvlem3  19779  reeff1olem  19822  logccv  20010  rlimcnp  20260  rlimcnp2  20261  jensenlem1  20281  jensenlem2  20282  jensen  20283  wilthlem2  20307  ppisval  20341  prmdvdsfi  20345  mumul  20419  sqff1o  20420  chtlepsi  20445  chpub  20459  dchrisum0lem2a  20666  pntlem3  20758  ex-res  20828  ghsubgolem  21037  htthlem  21497  chlejb1i  22055  ssmd2  22892  ballotlemsima  23074  iundisj2fi  23364  iundisj2f  23366  erdsze2lem2  23735  iccllyscon  23781  cvmscld  23804  cvmopnlem  23809  relexpdm  24032  relexprn  24033  nodenselem6  24340  nofulllem5  24360  islp3  25514  unint2t  25518  cmptdst  25568  supbrr  25636  prismorcsetlem  25912  prismorcset  25914  neiin  26250  neibastop1  26308  neibastop2lem  26309  topmeet  26313  sstotbnd2  26498  sstotbnd3  26500  ssbnd  26512  ismtyima  26527  heibor1lem  26533  isnacs2  26781  isnacs3  26785  diophrw  26838  pellfundre  26966  pellfundge  26967  pellfundlb  26969  pellfundglb  26970  fnwe2lem2  27148  lmhmfgima  27182  frlmsslsp  27248  lindff1  27290  lindfrn  27291  f1lindf  27292  lindfmm  27297  lsslindf  27300  hbt  27334  rngunsnply  27378  f1omvdconj  27389  f1omvdco2  27391  symgsssg  27408  symggen  27411  psgnunilem1  27416  cntzsdrg  27510  climinf  27732  stoweidlem27  27776  bnj1311  29054  lsatfixedN  29199  pmodlem2  30036  pmodN  30039  diaintclN  31248  djaclN  31326  dibintclN  31357  dicval  31366  dihoml4c  31566  djhcl  31590  dochsnkr  31662  hdmaprnlem4tN  32045
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator