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

Theorem syl6ss 3191
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 10 . 2  |-  ( ph  ->  B  C_  C )
41, 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:  difss2  3305  rintn0  3992  ssxpb  5110  relfld  5198  coexg  5215  funssxp  5402  dff2  5672  dff3  5673  fliftf  5814  1stcof  6147  2ndcof  6148  oacomf1olem  6562  nnunifi  7108  elfiun  7183  marypha1lem  7186  marypha1  7187  ordtypelem7  7239  tcmin  7426  unwf  7482  tcrank  7554  numacn  7676  aceq3lem  7747  dfac12lem2  7770  ackbij1lem9  7854  ackbij1lem10  7855  ackbij1lem16  7861  fin23lem26  7951  fin23lem27  7954  fin1a2lem6  8031  itunitc  8047  axdc3lem2  8077  ttukeylem5  8140  fpwwe2lem13  8264  canthwelem  8272  pwfseqlem4  8284  wunex2  8360  wunex3  8363  inar1  8397  inatsk  8400  gruina  8440  suprzub  10309  uzsupss  10310  uzwo3  10311  rpnnen1lem4  10345  rpnnen1lem5  10346  supxrre  10646  infmxrre  10654  ioodisj  10765  uzindi  11043  seqcoll  11401  seqcoll2  11402  limsupval2  11954  limsupgre  11955  limsupbnd2  11957  rlimuni  12024  rlimcld2  12052  rlimno1  12127  isercolllem2  12139  isercoll  12141  summolem2a  12188  summolem2  12189  fsumsers  12201  fsumcvg3  12202  4sqlem11  13002  vdwlem8  13035  vdwlem11  13038  ramub2  13061  0ram  13067  0ram2  13068  0ramcl  13070  ramub1lem1  13073  ramub1lem2  13074  isohom  13674  funcres2c  13775  resscntz  14807  cntzidss  14813  cntzmhm2  14815  pgpssslw  14925  cntzspan  15137  gsumval3  15191  gsum2d  15223  dprdspan  15262  dpjidcl  15293  lssintcl  15721  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  mplbas2  16212  fctop  16741  cctop  16743  clsval2  16787  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  lmss  17026  clscon  17156  2ndcdisj  17182  2ndcomap  17184  llycmpkgen2  17245  1stckgen  17249  ptbasfi  17276  txcmplem2  17336  hausdiag  17339  txkgen  17346  basqtop  17402  alexsublem  17738  alexsubb  17740  alexsubALTlem4  17744  tsmsres  17826  tsmsxplem1  17835  tsmsxp  17837  prdsmet  17934  icccmplem2  18328  xrge0tsms  18339  cnmptre  18425  icchmeo  18439  bndth  18456  lebnumlem2  18460  cfilresi  18721  causs  18724  bcthlem3  18748  bcthlem5  18750  evthicc  18819  ovolficcss  18829  ovolmge0  18836  ovolgelb  18839  ovollb2lem  18847  ovollb2  18848  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliunlem2  18862  ovoliun  18864  ovolscalem1  18872  ovolicc1  18875  ovolicc2lem4  18879  ovolicc2  18881  voliunlem2  18908  voliunlem3  18909  ioombl1lem2  18916  ioombl1lem4  18918  uniioovol  18934  uniiccvol  18935  uniioombllem1  18936  uniioombllem2  18938  uniioombllem3  18940  uniioombllem4  18941  uniioombllem6  18943  dyadmbllem  18954  dyadmbl  18955  volcn  18961  vitalilem4  18966  vitalilem5  18967  cnmbf  19014  i1fmul  19051  itg1addlem4  19054  itg2seq  19097  dvbssntr  19250  dvreslem  19259  dvcjbr  19298  dvferm1  19332  dvferm2  19334  cmvth  19338  dvlip  19340  lhop1lem  19360  lhop2  19362  lhop  19363  dvcnvrelem2  19365  dvcnvre  19366  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  ftc1a  19384  ftc1lem3  19385  ftc1lem6  19388  itgsubstlem  19395  mdegleb  19450  mdeglt  19451  mdegldg  19452  mdegxrcl  19453  mdegcl  19455  deg1mul3le  19502  ig1pdvds  19562  plyeq0lem  19592  aannenlem2  19709  aalioulem3  19714  taylf  19740  taylthlem2  19753  pserulm  19798  psercn2  19799  psercn  19802  reeff1olem  19822  efcvx  19825  loglesqr  20098  rlimcnp  20260  xrlimcnp  20263  jensen  20283  wilthlem2  20307  vmadivsumb  20632  pntrsumo1  20714  pntlem3  20758  nmoxr  21344  nmooge0  21345  nmoolb  21349  nmoubi  21350  ubthlem1  21449  shmodi  21969  nmopxr  22446  nmfnxr  22459  nmoplb  22487  nmopub  22488  nmfnlb  22504  nmfnleub  22505  nmopun  22594  branmfn  22685  mdslj1i  22899  hatomistici  22942  ballotlemsima  23074  suppss2f  23201  xppreima2  23212  fzssnn  23276  xrge0tsmsd  23382  sigaclci  23493  insiga  23498  rescon  23777  cvmliftlem8  23823  cvmlift3lem6  23855  nofulllem5  24360  axcontlem10  24601  areacirclem4  24927  areacirclem1  24928  areacirclem5  24929  uuniin  25087  basexre  25522  elsubops  25532  ivthALT  26258  neibastop1  26308  neibastop2lem  26309  topjoin  26314  totbndbnd  26513  prdsbnd  26517  heiborlem1  26535  rrnequiv  26559  reheibor  26563  iccbnd  26564  eldioph2lem2  26840  rmxyelqirr  26995  ttac  27129  islinds3  27304  hbtlem6  27333  hbt  27334  ibliccsinexp  27745  iblioosinexp  27747  usgraexmpl  28133  bnj1145  29023  bnj1137  29025  bnj1136  29027  pmapssbaN  29949  2polssN  30104  paddunN  30116  poldmj1N  30117  ispsubcl2N  30136  psubclinN  30137  paddatclN  30138  poml4N  30142  diaglbN  31245  diaintclN  31248  dibglbN  31356  dibintclN  31357  dicssdvh  31376  dihvalrel  31469  dochexmidlem4  31653
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