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

Theorem syl6ss 3362
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 3360 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3322
This theorem is referenced by:  difss2  3478  rintn0  4184  eqbrrdva  5045  ssxpb  5306  relfld  5398  funssxp  5607  dff2  5884  dff3  5885  fliftf  6040  1stcof  6377  2ndcof  6378  nnunifi  7361  elfiun  7438  marypha1lem  7441  marypha1  7442  ordtypelem7  7496  tcmin  7683  unwf  7739  rankfu  7806  tcrank  7813  aceq3lem  8006  dfac12lem2  8029  ackbij1lem9  8113  ackbij1lem10  8114  ackbij1lem16  8120  fin23lem26  8210  fin23lem27  8213  fin1a2lem6  8290  itunitc  8306  axdc3lem2  8336  ttukeylem5  8398  fpwwe2lem13  8522  canthwelem  8530  pwfseqlem4  8542  wunex2  8618  wunex3  8621  inar1  8655  inatsk  8658  gruina  8698  suprzub  10572  uzsupss  10573  uzwo3  10574  rpnnen1lem4  10608  rpnnen1lem5  10609  supxrre  10911  infmxrre  10919  ioodisj  11031  injresinjlem  11204  uzindi  11325  seqcoll  11717  seqcoll2  11718  limsupval2  12279  limsupgre  12280  limsupbnd2  12282  rlimuni  12349  rlimcld2  12377  rlimno1  12452  isercolllem2  12464  isercoll  12466  summolem2a  12514  summolem2  12515  fsumsers  12527  fsumcvg3  12528  4sqlem11  13328  vdwlem8  13361  vdwlem11  13364  ramub2  13387  0ram  13393  0ram2  13394  0ramcl  13396  ramub1lem2  13400  isohom  14002  funcres2c  14103  resscntz  15135  cntzidss  15141  cntzmhm2  15143  pgpssslw  15253  cntzspan  15465  gsumval3  15519  gsum2d  15551  dprdspan  15590  lssintcl  16045  lbsextlem2  16236  lbsextlem3  16237  lbsextlem4  16238  mplbas2  16536  fctop  17073  cctop  17075  neitr  17249  ordtbas2  17260  ordtopn1  17263  ordtopn2  17264  lmss  17367  clscon  17498  2ndcdisj  17524  2ndcomap  17526  ptbasfi  17618  txcmplem2  17679  hausdiag  17682  txkgen  17689  basqtop  17748  alexsubb  18082  alexsubALTlem4  18086  tsmsres  18178  tsmsxplem1  18187  tsmsxp  18189  ustrel  18246  utop3cls  18286  prdsmet  18405  metustrelOLD  18590  metustrel  18591  icccmplem2  18859  xrge0tsms  18870  cnmptre  18957  icchmeo  18971  bndth  18988  lebnumlem2  18992  cfilresi  19253  causs  19256  bcthlem5  19286  evthicc  19361  ovolficcss  19371  ovolmge0  19378  ovolgelb  19381  ovollb2lem  19389  ovollb2  19390  ovolunlem1a  19397  ovolunlem1  19398  ovoliunlem1  19403  ovoliunlem2  19404  ovoliun  19406  ovolscalem1  19414  ovolicc1  19417  ovolicc2lem4  19421  ovolicc2  19423  voliunlem2  19450  voliunlem3  19451  ioombl1lem2  19458  ioombl1lem4  19460  uniioovol  19476  uniiccvol  19477  uniioombllem1  19478  uniioombllem2  19480  uniioombllem3  19482  uniioombllem4  19483  uniioombllem6  19485  dyadmbllem  19496  dyadmbl  19497  volcn  19503  vitalilem4  19508  vitalilem5  19509  cnmbf  19554  i1fmul  19591  itg1addlem4  19594  itg2seq  19637  dvbssntr  19792  dvreslem  19801  dvcjbr  19840  dvferm1  19874  dvferm2  19876  cmvth  19880  dvlip  19882  lhop1lem  19902  lhop2  19904  lhop  19905  dvcnvrelem2  19907  dvcnvre  19908  dvfsumle  19910  dvfsumge  19911  dvfsumabs  19912  dvfsumlem2  19916  ftc1a  19926  ftc1lem3  19927  ftc1lem6  19930  itgsubstlem  19937  mdegleb  19992  mdeglt  19993  mdegldg  19994  mdegxrcl  19995  mdegcl  19997  deg1mul3le  20044  ig1pdvds  20104  plyeq0lem  20134  aannenlem2  20251  aalioulem3  20256  taylf  20282  taylthlem2  20295  pserulm  20343  psercn2  20344  psercn  20347  reeff1olem  20367  efcvx  20370  loglesqr  20647  rlimcnp  20809  xrlimcnp  20812  jensen  20832  wilthlem2  20857  vmadivsumb  21182  pntrsumo1  21264  pntlem3  21308  usgraexmpl  21425  nmoxr  22272  nmooge0  22273  nmoolb  22277  nmoubi  22278  ubthlem1  22377  shmodi  22897  nmopxr  23374  nmfnxr  23387  nmoplb  23415  nmopub  23416  nmfnlb  23432  nmfnleub  23433  nmopun  23522  branmfn  23613  mdslj1i  23827  hatomistici  23870  suppss2f  24054  xppreima2  24065  fzssnn  24152  xrge0tsmsd  24228  metideq  24293  metider  24294  pstmfval  24296  sigaclci  24520  insiga  24525  ballotlemsima  24778  rescon  24938  cvmliftlem8  24984  cvmlift3lem6  25016  prodmolem2a  25265  prodmolem2  25266  zprod  25268  nofulllem5  25666  axcontlem10  25917  heicant  26253  mblfinlem2  26256  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  itg2gt0cn  26274  ftc1cnnc  26293  ftc1anclem3  26296  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  areacirclem2  26307  areacirclem3  26308  areacirclem4  26309  ivthALT  26352  neibastop1  26402  topjoin  26408  totbndbnd  26512  prdsbnd  26516  heiborlem1  26534  rrnequiv  26558  reheibor  26562  iccbnd  26563  rmxyelqirr  26987  ttac  27121  islinds3  27295  hbtlem6  27324  hbt  27325  ibliccsinexp  27735  iblioosinexp  27737  stoweidlem34  27773  stoweidlem59  27798  fzossnn0  28147  bnj1145  29436  bnj1137  29438  bnj1136  29440  pmapssbaN  30631  2polssN  30786  paddunN  30798  poldmj1N  30799  ispsubcl2N  30818  psubclinN  30819  paddatclN  30820  poml4N  30824  diaglbN  31927  diaintclN  31930  dibglbN  32038  dibintclN  32039  dicssdvh  32058  dihvalrel  32151  dochexmidlem4  32335
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 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
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 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator