Theorem syl6ss 3615

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

Step	Hyp	Ref	Expression
1		syl6ss.1	. 2 |- ( ph -> A C_ B )
2		syl6ss.2	. . 3 |- B C_ C
3	2	a1i 11	. 2 |- ( ph -> B C_ C )
4	1, 3	sstrd 3613	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  difss2  3739  rintn0  4619  eqbrrdva  5291  ssxpb  5568  relfld  5661  funssxp  6061  dff2  6371  dff3  6372  fliftf  6565  1stcof  7196  2ndcof  7197  nnunifi  8211  elfiun  8336  marypha1lem  8339  marypha1  8340  ordtypelem7  8429  tcmin  8617  unwf  8673  rankfu  8740  tcrank  8747  aceq3lem  8943  dfac12lem2  8966  ackbij1lem9  9050  ackbij1lem10  9051  ackbij1lem16  9057  fin23lem26  9147  fin23lem27  9150  fin1a2lem6  9227  itunitc  9243  axdc3lem2  9273  ttukeylem5  9335  fpwwe2lem13  9464  canthwelem  9472  pwfseqlem4  9484  wunex2  9560  wunex3  9563  inar1  9597  inatsk  9600  gruina  9640  suprfinzcl  11492  suprzub  11779  uzsupss  11780  uzwo3  11783  rpnnen1lem4  11817  rpnnen1lem5  11818  rpnnen1lem4OLD  11823  rpnnen1lem5OLD  11824  supxrre  12157  infxrre  12166  ioodisj  12302  supicclub2  12323  fzssnn  12385  fzossnn0  12499  elfzom1elp1fzo  12534  injresinjlem  12588  uzindi  12781  ssnn0fi  12784  seqcoll  13248  seqcoll2  13249  reltrclfv  13758  relexpdmg  13782  relexpdm  13783  relexprng  13786  relexprn  13787  relexpfld  13789  relexpaddg  13793  limsupval2  14211  limsupgre  14212  limsupbnd2  14214  rlimuni  14281  rlimcld2  14309  rlimno1  14384  isercolllem2  14396  isercoll  14398  summolem2a  14446  summolem2  14447  fsumsers  14459  fsumcvg3  14460  prodmolem2a  14664  prodmolem2  14665  zprod  14667  lcmfnnval  15337  lcmfnncl  15342  4sqlem11  15659  vdwlem8  15692  vdwlem11  15695  ramub2  15718  0ram  15724  0ram2  15725  0ramcl  15727  ramub1lem2  15731  prmgaplem3  15757  prmgaplem4  15758  isohom  16436  funcres2c  16561  resscntz  17764  cntzidss  17770  cntzmhm2  17772  pgpssslw  18029  cntzspan  18247  gsumval3  18308  gsum2d  18371  dprdspan  18426  dprdres  18427  lssintcl  18964  lbsextlem2  19159  lbsextlem3  19160  lbsextlem4  19161  mplbas2  19470  islinds3  20173  fctop  20808  cctop  20810  neitr  20984  ordtbas2  20995  ordtopn1  20998  ordtopn2  20999  lmss  21102  clsconn  21233  2ndcdisj  21259  2ndcomap  21261  ptbasfi  21384  txcmplem2  21445  hausdiag  21448  txkgen  21455  basqtop  21514  alexsubb  21850  alexsubALTlem4  21854  tsmsres  21947  tsmsxplem1  21956  tsmsxp  21958  ustrel  22015  utop3cls  22055  prdsmet  22175  metustrel  22357  icccmplem2  22626  xrge0tsms  22637  cnmptre  22726  icchmeo  22740  bndth  22757  lebnumlem2  22761  cfilresi  23093  causs  23096  bcthlem5  23125  evthicc  23228  ovolficcss  23238  ovolmge0  23245  ovolgelb  23248  ovollb2lem  23256  ovollb2  23257  ovolunlem1a  23264  ovolunlem1  23265  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun  23273  ovolscalem1  23281  ovolicc1  23284  ovolicc2lem4  23288  ovolicc2  23290  voliunlem2  23319  voliunlem3  23320  ioombl1lem2  23327  ioombl1lem4  23329  uniioovol  23347  uniiccvol  23348  uniioombllem1  23349  uniioombllem2  23351  uniioombllem3  23353  uniioombllem4  23354  uniioombllem6  23356  dyadmbllem  23367  dyadmbl  23368  volcn  23374  vitalilem4  23380  vitalilem5  23381  cnmbf  23426  i1fmul  23463  itg1addlem4  23466  itg2seq  23509  dvbssntr  23664  dvreslem  23673  dvcjbr  23712  dvferm1  23748  dvferm2  23750  cmvth  23754  dvlip  23756  lhop1lem  23776  lhop2  23778  lhop  23779  dvcnvrelem2  23781  dvcnvre  23782  dvfsumle  23784  dvfsumge  23785  dvfsumabs  23786  dvfsumlem2  23790  ftc1a  23800  ftc1lem3  23801  ftc1lem6  23804  itgsubstlem  23811  mdegleb  23824  mdeglt  23825  mdegldg  23826  mdegxrcl  23827  mdegcl  23829  deg1mul3le  23876  ig1pdvds  23936  plyeq0lem  23966  aannenlem2  24084  aalioulem3  24089  taylf  24115  taylthlem2  24128  pserulm  24176  psercn2  24177  psercn  24180  reeff1olem  24200  efcvx  24203  loglesqrt  24499  rlimcnp  24692  xrlimcnp  24695  jensen  24715  wilthlem2  24795  vmadivsumb  25172  pntrsumo1  25254  pntlem3  25298  perpln2  25606  axcontlem10  25853  usgrexmplef  26151  nmoxr  27621  nmooge0  27622  nmoolb  27626  nmoubi  27627  ubthlem1  27726  shmodi  28249  nmopxr  28725  nmfnxr  28738  nmoplb  28766  nmopub  28767  nmfnlb  28783  nmfnleub  28784  nmopun  28873  branmfn  28964  mdslj1i  29178  hatomistici  29221  xppreima2  29450  fpwrelmap  29508  infxrge0gelb  29531  xrge0tsmsd  29785  metideq  29936  metider  29937  pstmfval  29939  esumgect  30152  esum2d  30155  sigaclci  30195  insiga  30200  omssubadd  30362  eulerpartlemgs2  30442  ballotlemsima  30577  signsply0  30628  iblidicc  30670  fsum2dsub  30685  reprsuc  30693  reprgt  30699  bnj1145  31061  bnj1137  31063  bnj1136  31065  resconn  31228  cvmliftlem8  31274  cvmlift3lem6  31306  mclsssvlem  31459  mclsind  31467  mclsppslem  31480  nosupbday  31851  ivthALT  32330  neibastop1  32354  topjoin  32360  ptrecube  33409  poimirlem6  33415  poimirlem15  33424  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2gt0cn  33465  ftc1cnnc  33484  ftc1anclem3  33487  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  areacirclem2  33501  areacirclem3  33502  areacirclem4  33503  totbndbnd  33588  prdsbnd  33592  heiborlem1  33610  rrnequiv  33634  reheibor  33638  iccbnd  33639  pmapssbaN  35046  2polssN  35201  paddunN  35213  poldmj1N  35214  ispsubcl2N  35233  psubclinN  35234  paddatclN  35235  poml4N  35239  diaglbN  36344  diaintclN  36347  dibglbN  36455  dibintclN  36456  dicssdvh  36475  dihvalrel  36568  dochexmidlem4  36752  rmxyelqirr  37475  ttac  37603  hbtlem6  37699  hbt  37700  itgpowd  37800  cnvssb  37892  cnvrcl0  37932  cnvtrrel  37962  relexpaddss  38010  cotrcltrcl  38017  cotrclrcl  38034  frege96d  38041  frege97d  38044  frege109d  38049  frege131d  38056  rp-imass  38065  rfovcnvf1od  38298  isotone2  38347  gneispace  38432  k0004ss1  38449  uzfissfz  39542  suplesup  39555  limciccioolb  39853  limcicciooub  39869  limcleqr  39876  cnrefiisplem  40055  cncfiooicclem1  40106  ibliccsinexp  40166  iblioosinexp  40168  itgcoscmulx  40185  itgsincmulx  40190  itgsubsticclem  40191  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem34  40251  stoweidlem59  40276  dirkeritg  40319  dirkercncflem2  40321  fourierdlem20  40344  fourierdlem31  40355  fourierdlem39  40363  fourierdlem42  40366  fourierdlem46  40369  fourierdlem52  40375  fourierdlem53  40376  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem68  40391  fourierdlem76  40399  fourierdlem85  40408  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem93  40416  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fouriersw  40448  etransclem46  40497  etransclem48  40499  sge0less  40609  sge0resplit  40623  sge0isum  40644  pimdecfgtioo  40927  pimincfltioo  40928  iccpartipre  41357  bgoldbtbndlem2  41694  setrec1lem4  42437  setrec2fun  42439