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

Theorem syl5ss 3327
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 11 . 2  |-  ( ph  ->  A  C_  B )
3 syl5ss.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3sstrd 3326 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3288
This theorem is referenced by:  wereu2  4547  sofld  5285  fvmptss  5780  fimacnv  5829  isofr2  6031  frxp  6423  fnse  6430  smores2  6583  f1imaen2g  7135  domunsncan  7175  fissuni  7377  fipreima  7378  dffi3  7402  marypha1lem  7404  ordtypelem7  7457  ordtypelem8  7458  oismo  7473  unxpwdom2  7520  oemapvali  7604  mapfien  7617  tskwe  7801  acndom2  7899  dfac2a  7974  dfac12lem2  7988  cfle  8098  cofsmo  8113  coftr  8117  isf34lem5  8222  isf34lem7  8223  isf34lem6  8224  enfin1ai  8228  fin1a2lem12  8255  ttukeylem7  8359  alephexp1  8418  fpwwe2lem13  8481  fpwwe2  8482  canth4  8486  canthwelem  8489  pwfseqlem1  8497  pwfseqlem4  8501  limsupgle  12234  limsupgre  12238  rlimres  12315  lo1res  12316  lo1resb  12321  rlimresb  12322  o1resb  12323  o1of2  12369  o1rlimmul  12375  isercolllem2  12422  isercoll  12424  climsup  12426  bitsinvp1  12924  sadcaddlem  12932  sadadd2lem  12934  sadadd3  12936  sadasslem  12945  sadeq  12947  bitsres  12948  smuval2  12957  smupval  12963  smueqlem  12965  smumul  12968  1arith  13258  isstruct2  13441  setscom  13460  ressress  13489  imasvscafn  13725  imasless  13728  mrcssv  13802  isacs1i  13845  mreacs  13846  acsfn  13847  isacs4lem  14557  isacs5lem  14558  mhmima  14726  cntzmhm  15100  efgval  15312  gsumzaddlem  15489  dmdprdd  15523  dprdfeq0  15543  dprdres  15549  dprdss  15550  dprdz  15551  subgdmdprd  15555  dprddisj2  15560  dprd2dlem1  15562  dprd2da  15563  dprd2d2  15565  dmdprdsplit2lem  15566  lmhmlsp  16088  lsppratlem4  16185  islbs3  16190  lbsextlem3  16195  mplcoe2  16493  mplind  16525  znleval  16798  basdif0  16981  tgcl  16997  ppttop  17034  epttop  17036  ntrin  17088  mretopd  17119  neiptoptop  17158  cnclsi  17298  cnconst2  17309  cnrest  17311  cnrest2  17312  cnpresti  17314  cnprest2  17316  fiuncmp  17429  connsub  17445  conima  17449  iunconlem  17451  1stcfb  17469  2ndc1stc  17475  2ndcdisj  17480  kgentopon  17531  llycmpkgen2  17543  1stckgenlem  17546  kgencn3  17551  ptclsg  17608  ptcnplem  17614  txtube  17633  hausdiag  17638  txkgen  17645  xkoco1cn  17650  xkoco2cn  17651  xkococnlem  17652  qtoptop2  17692  basqtop  17704  imastopn  17713  hmeores  17764  hmphdis  17789  ptcmpfi  17806  fbssfi  17830  filin  17847  infil  17856  fbasrn  17877  fgtr  17883  elfm  17940  imaelfm  17944  hausflim  17974  flimclslem  17977  fclscmp  18023  cnextcn  18059  tmdgsum2  18087  tgpconcomp  18103  tsmsres  18134  ustexsym  18206  ustund  18212  ustimasn  18219  utoptop  18225  utopbas  18226  restutopopn  18229  blin2  18420  metustexhalfOLD  18554  metustexhalf  18555  icccmplem2  18815  icccmplem3  18816  reconnlem2  18819  tchcph  19155  fmcfil  19186  resscdrg  19273  ivthlem2  19310  ivthlem3  19311  ivth2  19313  ovolfiniun  19358  ovoliunlem1  19359  ismbl2  19384  nulmbl2  19392  unmbl  19393  shftmbl  19394  voliunlem1  19405  voliunlem2  19406  ioombl1lem4  19416  uniioombllem4  19439  dyadmbllem  19452  dyadmbl  19453  mbflimsup  19519  i1fima  19531  i1fima2  19532  i1fadd  19548  itg1addlem4  19552  itg2splitlem  19601  itg2split  19602  ellimc3  19727  limcflflem  19728  limcflf  19729  limcresi  19733  limciun  19742  dvreslem  19757  dvres2lem  19758  dvres  19759  dvaddbr  19785  dvmulbr  19786  dvlip  19838  dvlip2  19840  c1liplem1  19841  dvivthlem1  19853  dvne0  19856  lhop1lem  19858  lhop  19861  dvcnvrelem1  19862  dvcnvrelem2  19863  dvfsumle  19866  dvfsumabs  19868  dvfsumlem2  19872  itgsubstlem  19893  mdegleb  19948  mdeglt  19949  mdegldg  19950  mdegxrcl  19951  mdegcl  19953  ig1peu  20055  reeff1olem  20323  logccv  20515  rlimcnp2  20766  ppisval  20847  prmdvdsfi  20851  mumul  20925  sqff1o  20926  chtlepsi  20951  chpub  20965  dchrisum0lem2a  21172  pntlem3  21264  ex-res  21710  ghsubgolem  21919  htthlem  22381  chlejb1i  22939  ssmd2  23776  sibfof  24615  sitgclbn  24618  ballotlemsima  24734  lgamgulmlem2  24775  erdsze2lem2  24851  iccllyscon  24898  cvmopnlem  24926  relexpdm  25096  relexprn  25097  fprodntriv  25229  nodenselem6  25562  nofulllem5  25582  cnambfre  26162  itg2gt0cn  26167  neiin  26233  neibastop1  26286  neibastop2lem  26287  topmeet  26291  sstotbnd2  26381  sstotbnd3  26383  ssbnd  26395  ismtyima  26410  heibor1lem  26416  isnacs2  26658  isnacs3  26662  diophrw  26715  pellfundre  26842  pellfundge  26843  pellfundlb  26845  pellfundglb  26846  fnwe2lem2  27024  lmhmfgima  27058  frlmsslsp  27124  lindff1  27166  lindfrn  27167  f1lindf  27168  lindfmm  27173  lsslindf  27176  hbt  27210  f1omvdconj  27265  f1omvdco2  27267  symgsssg  27284  symggen  27287  psgnunilem1  27292  climinf  27607  stoweidlem27  27651  swrdccatin12lem3c  28031  bnj1311  29111  pmodlem2  30341  pmodN  30344  diaintclN  31553  djaclN  31631  dibintclN  31662  dicval  31671  dihoml4c  31871  djhcl  31895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator