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

Theorem syl6ss 3320
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 3318 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3280
This theorem is referenced by:  difss2  3436  rintn0  4141  eqbrrdva  5001  ssxpb  5262  relfld  5354  funssxp  5563  dff2  5840  dff3  5841  fliftf  5996  1stcof  6333  2ndcof  6334  nnunifi  7317  elfiun  7393  marypha1lem  7396  marypha1  7397  ordtypelem7  7449  tcmin  7636  unwf  7692  tcrank  7764  aceq3lem  7957  dfac12lem2  7980  ackbij1lem9  8064  ackbij1lem10  8065  ackbij1lem16  8071  fin23lem26  8161  fin23lem27  8164  fin1a2lem6  8241  itunitc  8257  axdc3lem2  8287  ttukeylem5  8349  fpwwe2lem13  8473  canthwelem  8481  pwfseqlem4  8493  wunex2  8569  wunex3  8572  inar1  8606  inatsk  8609  gruina  8649  suprzub  10523  uzsupss  10524  uzwo3  10525  rpnnen1lem4  10559  rpnnen1lem5  10560  supxrre  10862  infmxrre  10870  ioodisj  10982  injresinjlem  11154  uzindi  11275  seqcoll  11667  seqcoll2  11668  limsupval2  12229  limsupgre  12230  limsupbnd2  12232  rlimuni  12299  rlimcld2  12327  rlimno1  12402  isercolllem2  12414  isercoll  12416  summolem2a  12464  summolem2  12465  fsumsers  12477  fsumcvg3  12478  4sqlem11  13278  vdwlem8  13311  vdwlem11  13314  ramub2  13337  0ram  13343  0ram2  13344  0ramcl  13346  ramub1lem2  13350  isohom  13952  funcres2c  14053  resscntz  15085  cntzidss  15091  cntzmhm2  15093  pgpssslw  15203  cntzspan  15415  gsumval3  15469  gsum2d  15501  dprdspan  15540  lssintcl  15995  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  mplbas2  16486  fctop  17023  cctop  17025  neitr  17198  ordtbas2  17209  ordtopn1  17212  ordtopn2  17213  lmss  17316  clscon  17446  2ndcdisj  17472  2ndcomap  17474  ptbasfi  17566  txcmplem2  17627  hausdiag  17630  txkgen  17637  basqtop  17696  alexsubb  18030  alexsubALTlem4  18034  tsmsres  18126  tsmsxplem1  18135  tsmsxp  18137  ustrel  18194  utop3cls  18234  prdsmet  18353  metustrelOLD  18538  metustrel  18539  icccmplem2  18807  xrge0tsms  18818  cnmptre  18905  icchmeo  18919  bndth  18936  lebnumlem2  18940  cfilresi  19201  causs  19204  bcthlem5  19234  evthicc  19309  ovolficcss  19319  ovolmge0  19326  ovolgelb  19329  ovollb2lem  19337  ovollb2  19338  ovolunlem1a  19345  ovolunlem1  19346  ovoliunlem1  19351  ovoliunlem2  19352  ovoliun  19354  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem4  19369  ovolicc2  19371  voliunlem2  19398  voliunlem3  19399  ioombl1lem2  19406  ioombl1lem4  19408  uniioovol  19424  uniiccvol  19425  uniioombllem1  19426  uniioombllem2  19428  uniioombllem3  19430  uniioombllem4  19431  uniioombllem6  19433  dyadmbllem  19444  dyadmbl  19445  volcn  19451  vitalilem4  19456  vitalilem5  19457  cnmbf  19504  i1fmul  19541  itg1addlem4  19544  itg2seq  19587  dvbssntr  19740  dvreslem  19749  dvcjbr  19788  dvferm1  19822  dvferm2  19824  cmvth  19828  dvlip  19830  lhop1lem  19850  lhop2  19852  lhop  19853  dvcnvrelem2  19855  dvcnvre  19856  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  ftc1a  19874  ftc1lem3  19875  ftc1lem6  19878  itgsubstlem  19885  mdegleb  19940  mdeglt  19941  mdegldg  19942  mdegxrcl  19943  mdegcl  19945  deg1mul3le  19992  ig1pdvds  20052  plyeq0lem  20082  aannenlem2  20199  aalioulem3  20204  taylf  20230  taylthlem2  20243  pserulm  20291  psercn2  20292  psercn  20295  reeff1olem  20315  efcvx  20318  loglesqr  20595  rlimcnp  20757  xrlimcnp  20760  jensen  20780  wilthlem2  20805  vmadivsumb  21130  pntrsumo1  21212  pntlem3  21256  usgraexmpl  21373  nmoxr  22220  nmooge0  22221  nmoolb  22225  nmoubi  22226  ubthlem1  22325  shmodi  22845  nmopxr  23322  nmfnxr  23335  nmoplb  23363  nmopub  23364  nmfnlb  23380  nmfnleub  23381  nmopun  23470  branmfn  23561  mdslj1i  23775  hatomistici  23818  suppss2f  24002  xppreima2  24013  fzssnn  24100  xrge0tsmsd  24176  metideq  24241  metider  24242  pstmfval  24244  sigaclci  24468  insiga  24473  ballotlemsima  24726  rescon  24886  cvmliftlem8  24932  cvmlift3lem6  24964  prodmolem2a  25213  prodmolem2  25214  zprod  25216  nofulllem5  25574  axcontlem10  25816  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  itg2gt0cn  26159  ftc1cnnc  26178  areacirclem4  26183  areacirclem1  26184  areacirclem5  26185  ivthALT  26228  neibastop1  26278  topjoin  26284  totbndbnd  26388  prdsbnd  26392  heiborlem1  26410  rrnequiv  26434  reheibor  26438  iccbnd  26439  rmxyelqirr  26863  ttac  26997  islinds3  27172  hbtlem6  27201  hbt  27202  ibliccsinexp  27612  iblioosinexp  27614  stoweidlem34  27650  stoweidlem59  27675  swrdccatin12  28026  bnj1145  29068  bnj1137  29070  bnj1136  29072  pmapssbaN  30242  2polssN  30397  paddunN  30409  poldmj1N  30410  ispsubcl2N  30429  psubclinN  30430  paddatclN  30431  poml4N  30435  diaglbN  31538  diaintclN  31541  dibglbN  31649  dibintclN  31650  dicssdvh  31669  dihvalrel  31762  dochexmidlem4  31946
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 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator