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

Theorem syl6ss 3352
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl6ss.1  |-  ( ph  ->  A  C_  B )
syl6ss.2  |-  B  C_  C
Assertion
Ref Expression
syl6ss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl6ss
StepHypRef Expression
1 syl6ss.1 . 2  |-  ( ph  ->  A  C_  B )
2 syl6ss.2 . . 3  |-  B  C_  C
32a1i 11 . 2  |-  ( ph  ->  B  C_  C )
41, 3sstrd 3350 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3312
This theorem is referenced by:  difss2  3468  rintn0  4173  eqbrrdva  5034  ssxpb  5295  relfld  5387  funssxp  5596  dff2  5873  dff3  5874  fliftf  6029  1stcof  6366  2ndcof  6367  nnunifi  7350  elfiun  7427  marypha1lem  7430  marypha1  7431  ordtypelem7  7485  tcmin  7672  unwf  7728  tcrank  7800  aceq3lem  7993  dfac12lem2  8016  ackbij1lem9  8100  ackbij1lem10  8101  ackbij1lem16  8107  fin23lem26  8197  fin23lem27  8200  fin1a2lem6  8277  itunitc  8293  axdc3lem2  8323  ttukeylem5  8385  fpwwe2lem13  8509  canthwelem  8517  pwfseqlem4  8529  wunex2  8605  wunex3  8608  inar1  8642  inatsk  8645  gruina  8685  suprzub  10559  uzsupss  10560  uzwo3  10561  rpnnen1lem4  10595  rpnnen1lem5  10596  supxrre  10898  infmxrre  10906  ioodisj  11018  injresinjlem  11191  uzindi  11312  seqcoll  11704  seqcoll2  11705  limsupval2  12266  limsupgre  12267  limsupbnd2  12269  rlimuni  12336  rlimcld2  12364  rlimno1  12439  isercolllem2  12451  isercoll  12453  summolem2a  12501  summolem2  12502  fsumsers  12514  fsumcvg3  12515  4sqlem11  13315  vdwlem8  13348  vdwlem11  13351  ramub2  13374  0ram  13380  0ram2  13381  0ramcl  13383  ramub1lem2  13387  isohom  13989  funcres2c  14090  resscntz  15122  cntzidss  15128  cntzmhm2  15130  pgpssslw  15240  cntzspan  15452  gsumval3  15506  gsum2d  15538  dprdspan  15577  lssintcl  16032  lbsextlem2  16223  lbsextlem3  16224  lbsextlem4  16225  mplbas2  16523  fctop  17060  cctop  17062  neitr  17236  ordtbas2  17247  ordtopn1  17250  ordtopn2  17251  lmss  17354  clscon  17485  2ndcdisj  17511  2ndcomap  17513  ptbasfi  17605  txcmplem2  17666  hausdiag  17669  txkgen  17676  basqtop  17735  alexsubb  18069  alexsubALTlem4  18073  tsmsres  18165  tsmsxplem1  18174  tsmsxp  18176  ustrel  18233  utop3cls  18273  prdsmet  18392  metustrelOLD  18577  metustrel  18578  icccmplem2  18846  xrge0tsms  18857  cnmptre  18944  icchmeo  18958  bndth  18975  lebnumlem2  18979  cfilresi  19240  causs  19243  bcthlem5  19273  evthicc  19348  ovolficcss  19358  ovolmge0  19365  ovolgelb  19368  ovollb2lem  19376  ovollb2  19377  ovolunlem1a  19384  ovolunlem1  19385  ovoliunlem1  19390  ovoliunlem2  19391  ovoliun  19393  ovolscalem1  19401  ovolicc1  19404  ovolicc2lem4  19408  ovolicc2  19410  voliunlem2  19437  voliunlem3  19438  ioombl1lem2  19445  ioombl1lem4  19447  uniioovol  19463  uniiccvol  19464  uniioombllem1  19465  uniioombllem2  19467  uniioombllem3  19469  uniioombllem4  19470  uniioombllem6  19472  dyadmbllem  19483  dyadmbl  19484  volcn  19490  vitalilem4  19495  vitalilem5  19496  cnmbf  19543  i1fmul  19580  itg1addlem4  19583  itg2seq  19626  dvbssntr  19779  dvreslem  19788  dvcjbr  19827  dvferm1  19861  dvferm2  19863  cmvth  19867  dvlip  19869  lhop1lem  19889  lhop2  19891  lhop  19892  dvcnvrelem2  19894  dvcnvre  19895  dvfsumle  19897  dvfsumge  19898  dvfsumabs  19899  dvfsumlem2  19903  ftc1a  19913  ftc1lem3  19914  ftc1lem6  19917  itgsubstlem  19924  mdegleb  19979  mdeglt  19980  mdegldg  19981  mdegxrcl  19982  mdegcl  19984  deg1mul3le  20031  ig1pdvds  20091  plyeq0lem  20121  aannenlem2  20238  aalioulem3  20243  taylf  20269  taylthlem2  20282  pserulm  20330  psercn2  20331  psercn  20334  reeff1olem  20354  efcvx  20357  loglesqr  20634  rlimcnp  20796  xrlimcnp  20799  jensen  20819  wilthlem2  20844  vmadivsumb  21169  pntrsumo1  21251  pntlem3  21295  usgraexmpl  21412  nmoxr  22259  nmooge0  22260  nmoolb  22264  nmoubi  22265  ubthlem1  22364  shmodi  22884  nmopxr  23361  nmfnxr  23374  nmoplb  23402  nmopub  23403  nmfnlb  23419  nmfnleub  23420  nmopun  23509  branmfn  23600  mdslj1i  23814  hatomistici  23857  suppss2f  24041  xppreima2  24052  fzssnn  24139  xrge0tsmsd  24215  metideq  24280  metider  24281  pstmfval  24283  sigaclci  24507  insiga  24512  ballotlemsima  24765  rescon  24925  cvmliftlem8  24971  cvmlift3lem6  25003  prodmolem2a  25252  prodmolem2  25253  zprod  25255  nofulllem5  25653  axcontlem10  25904  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  itg2gt0cn  26250  ftc1cnnc  26269  ftc1anclem3  26272  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  areacirclem4  26284  areacirclem1  26285  areacirclem5  26286  ivthALT  26329  neibastop1  26379  topjoin  26385  totbndbnd  26489  prdsbnd  26493  heiborlem1  26511  rrnequiv  26535  reheibor  26539  iccbnd  26540  rmxyelqirr  26964  ttac  27098  islinds3  27272  hbtlem6  27301  hbt  27302  ibliccsinexp  27712  iblioosinexp  27714  stoweidlem34  27750  stoweidlem59  27775  fzossnn0  28107  bnj1145  29299  bnj1137  29301  bnj1136  29303  pmapssbaN  30494  2polssN  30649  paddunN  30661  poldmj1N  30662  ispsubcl2N  30681  psubclinN  30682  paddatclN  30683  poml4N  30687  diaglbN  31790  diaintclN  31793  dibglbN  31901  dibintclN  31902  dicssdvh  31921  dihvalrel  32014  dochexmidlem4  32198
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