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

Theorem syl5ss 3203
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 3202 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3165
This theorem is referenced by:  wereu2  4406  sofld  5137  fvmptss  5625  fimacnv  5673  isofr2  5857  frxp  6241  fnse  6248  smores2  6387  ersym  6688  ertr  6691  f1imaen2g  6938  domunsncan  6978  fissuni  7176  fipreima  7177  finsschain  7178  dffi3  7200  marypha1lem  7202  ordtypelem7  7255  ordtypelem8  7256  oismo  7271  unxpwdom2  7318  oemapvali  7402  mapfien  7415  tskwe  7599  r0weon  7656  acndom2  7697  dfac2a  7772  dfac12lem2  7786  ackbij1lem16  7877  cfle  7896  cofsmo  7911  coftr  7915  fin23lem26  7967  fin23lem29  7983  isf32lem8  8002  isf34lem5  8020  isf34lem7  8021  isf34lem6  8022  enfin1ai  8026  fin1a2lem12  8053  ttukeylem7  8158  alephexp1  8217  fpwwe2lem13  8280  fpwwe2  8281  canth4  8285  canthwelem  8288  pwfseqlem1  8296  pwfseqlem4  8300  wunfi  8359  wunex2  8376  hashf1lem2  11410  limsupgle  11967  limsupgre  11971  rlimres  12048  lo1res  12049  lo1resb  12054  rlimresb  12055  o1resb  12056  o1of2  12102  o1rlimmul  12108  isercolllem2  12155  isercoll  12157  climsup  12159  sumsplit  12247  fsum2dlem  12249  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  bitsinvp1  12656  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  sadasslem  12677  sadeq  12679  bitsres  12680  smuval2  12689  smupval  12695  smueqlem  12697  smumul  12700  1arith  12990  isstruct2  13173  setscom  13192  ressress  13221  imasvscafn  13455  imasless  13458  mrcssv  13532  isacs1i  13575  mreacs  13576  acsfn  13577  yonedalem1  14062  yonedalem21  14063  yonedalem3a  14064  yonedalem4c  14067  yonedalem22  14068  yonedalem3b  14069  yonedainv  14071  yonffthlem  14072  isacs4lem  14287  isacs5lem  14288  mhmima  14456  cntzmhm  14830  efgval  15042  gsumzaddlem  15219  dmdprdd  15253  dprdfeq0  15273  dprdres  15279  dprdss  15280  dprdz  15281  subgdmdprd  15285  dprddisj2  15290  dprd2dlem1  15292  dprd2da  15293  dprd2d2  15295  dmdprdsplit2lem  15296  ablfac1eulem  15323  lmhmlsp  15822  lbspss  15851  lsmsp  15855  lspsolv  15912  lsppratlem3  15918  lsppratlem4  15919  lspprat  15922  islbs2  15923  islbs3  15924  lbsextlem2  15928  lbsextlem3  15929  lbsextlem4  15930  mplcoe1  16225  mplcoe2  16227  mplind  16259  znleval  16524  basdif0  16707  tgcl  16723  ppttop  16760  epttop  16762  ntrin  16814  mretopd  16845  lpss3  16892  restlp  16929  ordtbas  16938  cnclsi  17017  cnconst2  17027  cnrest  17029  cnrest2  17030  cnpresti  17032  cnprest2  17034  lpcls  17108  fiuncmp  17147  connsub  17163  conima  17167  iunconlem  17169  1stcfb  17187  2ndc1stc  17193  2ndcdisj  17198  kgentopon  17249  llycmpkgen2  17261  1stckgenlem  17264  kgencn3  17269  ptclsg  17325  ptcnplem  17331  txtube  17350  hausdiag  17355  txkgen  17362  xkoco1cn  17367  xkoco2cn  17368  xkococnlem  17369  qtoptop2  17406  basqtop  17418  qtoprest  17424  imastopn  17427  hmeores  17478  hmphdis  17503  ptcmpfi  17520  fbssfi  17548  filin  17565  infil  17574  fbasrn  17595  fgtr  17601  isufil2  17619  ufileu  17630  filufint  17631  ufinffr  17640  elfm  17658  imaelfm  17662  fmfnfmlem4  17668  fmfnfm  17669  hausflim  17692  flimclslem  17695  fclsfnflim  17738  flimfnfcls  17739  fclscmp  17741  tmdgsum2  17795  cldsubg  17809  tgpconcomp  17811  tsmsres  17842  imasdsf1olem  17953  blin2  17991  icccmplem2  18344  icccmplem3  18345  reconnlem2  18348  xrge0gsumle  18354  fsumcn  18390  tchcph  18683  fmcfil  18714  bcthlem5  18766  resscdrg  18791  ivthlem2  18828  ivthlem3  18829  ivth2  18831  ovolfiniun  18876  ovoliunlem1  18877  ismbl2  18902  cmmbl  18908  nulmbl2  18910  unmbl  18911  shftmbl  18912  iundisj2  18922  voliunlem1  18923  voliunlem2  18924  ioombl1lem4  18934  uniiccdif  18949  uniioombllem4  18957  uniiccmbl  18961  dyadmbllem  18970  dyadmbl  18971  mbflimsup  19037  i1fima  19049  i1fima2  19050  itg1val2  19055  itg1cl  19056  itg1ge0  19057  i1fadd  19066  itg1addlem4  19070  itg1addlem5  19071  i1fmulc  19074  itg1mulc  19075  itg10a  19081  itg1ge0a  19082  itg1climres  19085  mbfi1fseqlem4  19089  itg2splitlem  19119  itg2split  19120  itgss3  19185  itgfsum  19197  limcdif  19242  limcnlp  19244  ellimc3  19245  limcflflem  19246  limcflf  19247  limcmpt2  19250  limcresi  19251  limciun  19260  perfdvf  19269  dvreslem  19275  dvres2lem  19276  dvres  19277  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvferm1  19348  dvferm2  19350  dvlip  19356  dvlip2  19358  c1liplem1  19359  dvivthlem1  19371  dvne0  19374  lhop1lem  19376  lhop  19379  dvcnvrelem1  19380  dvcnvrelem2  19381  dvfsumle  19384  dvfsumabs  19386  dvfsumlem2  19390  ftc1lem6  19404  itgsubstlem  19411  mdegleb  19466  mdeglt  19467  mdegldg  19468  mdegxrcl  19469  mdegcl  19471  ig1peu  19573  ig1pdvds  19578  taylthlem1  19768  taylthlem2  19769  ulmdvlem3  19795  reeff1olem  19838  logccv  20026  rlimcnp  20276  rlimcnp2  20277  jensenlem1  20297  jensenlem2  20298  jensen  20299  wilthlem2  20323  ppisval  20357  prmdvdsfi  20361  mumul  20435  sqff1o  20436  chtlepsi  20461  chpub  20475  dchrisum0lem2a  20682  pntlem3  20774  ex-res  20844  ghsubgolem  21053  htthlem  21513  chlejb1i  22071  ssmd2  22908  ballotlemsima  23090  iundisj2fi  23379  iundisj2f  23381  erdsze2lem2  23750  iccllyscon  23796  cvmscld  23819  cvmopnlem  23824  relexpdm  24047  relexprn  24048  nodenselem6  24411  nofulllem5  24431  itg2gt0cn  25006  islp3  25617  unint2t  25621  cmptdst  25671  supbrr  25739  prismorcsetlem  26015  prismorcset  26017  neiin  26353  neibastop1  26411  neibastop2lem  26412  topmeet  26416  sstotbnd2  26601  sstotbnd3  26603  ssbnd  26615  ismtyima  26630  heibor1lem  26636  isnacs2  26884  isnacs3  26888  diophrw  26941  pellfundre  27069  pellfundge  27070  pellfundlb  27072  pellfundglb  27073  fnwe2lem2  27251  lmhmfgima  27285  frlmsslsp  27351  lindff1  27393  lindfrn  27394  f1lindf  27395  lindfmm  27400  lsslindf  27403  hbt  27437  rngunsnply  27481  f1omvdconj  27492  f1omvdco2  27494  symgsssg  27511  symggen  27514  psgnunilem1  27519  cntzsdrg  27613  climinf  27835  stoweidlem27  27879  bnj1311  29370  lsatfixedN  29821  pmodlem2  30658  pmodN  30661  diaintclN  31870  djaclN  31948  dibintclN  31979  dicval  31988  dihoml4c  32188  djhcl  32212  dochsnkr  32284  hdmaprnlem4tN  32667
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator