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

Theorem syl6ss 3346
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 3344 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3306
This theorem is referenced by:  difss2  3462  rintn0  4206  eqbrrdva  5071  ssxpb  5332  relfld  5424  funssxp  5633  dff2  5910  dff3  5911  fliftf  6066  1stcof  6403  2ndcof  6404  nnunifi  7387  elfiun  7464  marypha1lem  7467  marypha1  7468  ordtypelem7  7522  tcmin  7709  unwf  7765  rankfu  7832  tcrank  7839  aceq3lem  8032  dfac12lem2  8055  ackbij1lem9  8139  ackbij1lem10  8140  ackbij1lem16  8146  fin23lem26  8236  fin23lem27  8239  fin1a2lem6  8316  itunitc  8332  axdc3lem2  8362  ttukeylem5  8424  fpwwe2lem13  8548  canthwelem  8556  pwfseqlem4  8568  wunex2  8644  wunex3  8647  inar1  8681  inatsk  8684  gruina  8724  suprzub  10598  uzsupss  10599  uzwo3  10600  rpnnen1lem4  10634  rpnnen1lem5  10635  supxrre  10937  infmxrre  10945  ioodisj  11057  injresinjlem  11230  uzindi  11351  seqcoll  11743  seqcoll2  11744  limsupval2  12305  limsupgre  12306  limsupbnd2  12308  rlimuni  12375  rlimcld2  12403  rlimno1  12478  isercolllem2  12490  isercoll  12492  summolem2a  12540  summolem2  12541  fsumsers  12553  fsumcvg3  12554  4sqlem11  13354  vdwlem8  13387  vdwlem11  13390  ramub2  13413  0ram  13419  0ram2  13420  0ramcl  13422  ramub1lem2  13426  isohom  14028  funcres2c  14129  resscntz  15161  cntzidss  15167  cntzmhm2  15169  pgpssslw  15279  cntzspan  15491  gsumval3  15545  gsum2d  15577  dprdspan  15616  lssintcl  16071  lbsextlem2  16262  lbsextlem3  16263  lbsextlem4  16264  mplbas2  16562  fctop  17099  cctop  17101  neitr  17275  ordtbas2  17286  ordtopn1  17289  ordtopn2  17290  lmss  17393  clscon  17524  2ndcdisj  17550  2ndcomap  17552  ptbasfi  17644  txcmplem2  17705  hausdiag  17708  txkgen  17715  basqtop  17774  alexsubb  18108  alexsubALTlem4  18112  tsmsres  18204  tsmsxplem1  18213  tsmsxp  18215  ustrel  18272  utop3cls  18312  prdsmet  18431  metustrelOLD  18616  metustrel  18617  icccmplem2  18885  xrge0tsms  18896  cnmptre  18983  icchmeo  18997  bndth  19014  lebnumlem2  19018  cfilresi  19279  causs  19282  bcthlem5  19312  evthicc  19387  ovolficcss  19397  ovolmge0  19404  ovolgelb  19407  ovollb2lem  19415  ovollb2  19416  ovolunlem1a  19423  ovolunlem1  19424  ovoliunlem1  19429  ovoliunlem2  19430  ovoliun  19432  ovolscalem1  19440  ovolicc1  19443  ovolicc2lem4  19447  ovolicc2  19449  voliunlem2  19476  voliunlem3  19477  ioombl1lem2  19484  ioombl1lem4  19486  uniioovol  19502  uniiccvol  19503  uniioombllem1  19504  uniioombllem2  19506  uniioombllem3  19508  uniioombllem4  19509  uniioombllem6  19511  dyadmbllem  19522  dyadmbl  19523  volcn  19529  vitalilem4  19534  vitalilem5  19535  cnmbf  19580  i1fmul  19617  itg1addlem4  19620  itg2seq  19663  dvbssntr  19818  dvreslem  19827  dvcjbr  19866  dvferm1  19900  dvferm2  19902  cmvth  19906  dvlip  19908  lhop1lem  19928  lhop2  19930  lhop  19931  dvcnvrelem2  19933  dvcnvre  19934  dvfsumle  19936  dvfsumge  19937  dvfsumabs  19938  dvfsumlem2  19942  ftc1a  19952  ftc1lem3  19953  ftc1lem6  19956  itgsubstlem  19963  mdegleb  20018  mdeglt  20019  mdegldg  20020  mdegxrcl  20021  mdegcl  20023  deg1mul3le  20070  ig1pdvds  20130  plyeq0lem  20160  aannenlem2  20277  aalioulem3  20282  taylf  20308  taylthlem2  20321  pserulm  20369  psercn2  20370  psercn  20373  reeff1olem  20393  efcvx  20396  loglesqr  20673  rlimcnp  20835  xrlimcnp  20838  jensen  20858  wilthlem2  20883  vmadivsumb  21208  pntrsumo1  21290  pntlem3  21334  usgraexmpl  21451  nmoxr  22298  nmooge0  22299  nmoolb  22303  nmoubi  22304  ubthlem1  22403  shmodi  22923  nmopxr  23400  nmfnxr  23413  nmoplb  23441  nmopub  23442  nmfnlb  23458  nmfnleub  23459  nmopun  23548  branmfn  23639  mdslj1i  23853  hatomistici  23896  suppss2f  24080  xppreima2  24091  fzssnn  24178  xrge0tsmsd  24254  metideq  24319  metider  24320  pstmfval  24322  sigaclci  24546  insiga  24551  ballotlemsima  24804  rescon  24964  cvmliftlem8  25010  cvmlift3lem6  25042  prodmolem2a  25291  prodmolem2  25292  zprod  25294  nofulllem5  25692  axcontlem10  25943  heicant  26277  mblfinlem2  26280  mblfinlem3  26281  mblfinlem4  26282  ismblfin  26283  itg2gt0cn  26298  ftc1cnnc  26317  ftc1anclem3  26320  ftc1anclem7  26324  ftc1anclem8  26325  ftc1anc  26326  areacirclem2  26331  areacirclem3  26332  areacirclem4  26333  ivthALT  26376  neibastop1  26426  topjoin  26432  totbndbnd  26536  prdsbnd  26540  heiborlem1  26558  rrnequiv  26582  reheibor  26586  iccbnd  26587  rmxyelqirr  27011  ttac  27145  islinds3  27319  hbtlem6  27348  hbt  27349  ibliccsinexp  27759  iblioosinexp  27761  stoweidlem34  27797  stoweidlem59  27822  fzossnn0  28171  bnj1145  29460  bnj1137  29462  bnj1136  29464  pmapssbaN  30655  2polssN  30810  paddunN  30822  poldmj1N  30823  ispsubcl2N  30842  psubclinN  30843  paddatclN  30844  poml4N  30848  diaglbN  31951  diaintclN  31954  dibglbN  32062  dibintclN  32063  dicssdvh  32082  dihvalrel  32175  dochexmidlem4  32359
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3313  df-ss 3320
  Copyright terms: Public domain W3C validator