Theorem syl6ss 3580

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
syl6ss.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
syl6ss.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
syl6ss	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl6ss

Step	Hyp	Ref	Expression
1		syl6ss.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		syl6ss.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	1, 3	sstrd 3578	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  difss2  3701  rintn0  4552  eqbrrdva  5213  ssxpb  5487  relfld  5578  funssxp  5974  dff2  6279  dff3  6280  fliftf  6465  1stcof  7087  2ndcof  7088  nnunifi  8096  elfiun  8219  marypha1lem  8222  marypha1  8223  ordtypelem7  8312  tcmin  8500  unwf  8556  rankfu  8623  tcrank  8630  aceq3lem  8826  dfac12lem2  8849  ackbij1lem9  8933  ackbij1lem10  8934  ackbij1lem16  8940  fin23lem26  9030  fin23lem27  9033  fin1a2lem6  9110  itunitc  9126  axdc3lem2  9156  ttukeylem5  9218  fpwwe2lem13  9343  canthwelem  9351  pwfseqlem4  9363  wunex2  9439  wunex3  9442  inar1  9476  inatsk  9479  gruina  9519  suprfinzcl  11368  suprzub  11655  uzsupss  11656  uzwo3  11659  rpnnen1lem4  11693  rpnnen1lem5  11694  rpnnen1lem4OLD  11699  rpnnen1lem5OLD  11700  supxrre  12029  infxrre  12038  ioodisj  12173  supicclub2  12194  fzssnn  12256  fzossnn0  12368  elfzom1elp1fzo  12402  injresinjlem  12450  uzindi  12643  ssnn0fi  12646  seqcoll  13105  seqcoll2  13106  reltrclfv  13606  relexpdmg  13630  relexpdm  13631  relexprng  13634  relexprn  13635  relexpfld  13637  relexpaddg  13641  limsupval2  14059  limsupgre  14060  limsupbnd2  14062  rlimuni  14129  rlimcld2  14157  rlimno1  14232  isercolllem2  14244  isercoll  14246  summolem2a  14293  summolem2  14294  fsumsers  14306  fsumcvg3  14307  prodmolem2a  14503  prodmolem2  14504  zprod  14506  lcmfnnval  15175  lcmfnncl  15180  4sqlem11  15497  vdwlem8  15530  vdwlem11  15533  ramub2  15556  0ram  15562  0ram2  15563  0ramcl  15565  ramub1lem2  15569  prmgaplem3  15595  prmgaplem4  15596  isohom  16259  funcres2c  16384  resscntz  17587  cntzidss  17593  cntzmhm2  17595  pgpssslw  17852  cntzspan  18070  gsumval3  18131  gsum2d  18194  dprdspan  18249  dprdres  18250  lssintcl  18785  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  mplbas2  19291  islinds3  19992  fctop  20618  cctop  20620  neitr  20794  ordtbas2  20805  ordtopn1  20808  ordtopn2  20809  lmss  20912  clscon  21043  2ndcdisj  21069  2ndcomap  21071  ptbasfi  21194  txcmplem2  21255  hausdiag  21258  txkgen  21265  basqtop  21324  alexsubb  21660  alexsubALTlem4  21664  tsmsres  21757  tsmsxplem1  21766  tsmsxp  21768  ustrel  21825  utop3cls  21865  prdsmet  21985  metustrel  22167  icccmplem2  22434  xrge0tsms  22445  cnmptre  22534  icchmeo  22548  bndth  22565  lebnumlem2  22569  cfilresi  22901  causs  22904  bcthlem5  22933  evthicc  23035  ovolficcss  23045  ovolmge0  23052  ovolgelb  23055  ovollb2lem  23063  ovollb2  23064  ovolunlem1a  23071  ovolunlem1  23072  ovoliunlem1  23077  ovoliunlem2  23078  ovoliun  23080  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem4  23095  ovolicc2  23097  voliunlem2  23126  voliunlem3  23127  ioombl1lem2  23134  ioombl1lem4  23136  uniioovol  23153  uniiccvol  23154  uniioombllem1  23155  uniioombllem2  23157  uniioombllem3  23159  uniioombllem4  23160  uniioombllem6  23162  dyadmbllem  23173  dyadmbl  23174  volcn  23180  vitalilem4  23186  vitalilem5  23187  cnmbf  23232  i1fmul  23269  itg1addlem4  23272  itg2seq  23315  dvbssntr  23470  dvreslem  23479  dvcjbr  23518  dvferm1  23552  dvferm2  23554  cmvth  23558  dvlip  23560  lhop1lem  23580  lhop2  23582  lhop  23583  dvcnvrelem2  23585  dvcnvre  23586  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  dvfsumlem2  23594  ftc1a  23604  ftc1lem3  23605  ftc1lem6  23608  itgsubstlem  23615  mdegleb  23628  mdeglt  23629  mdegldg  23630  mdegxrcl  23631  mdegcl  23633  deg1mul3le  23680  ig1pdvds  23740  plyeq0lem  23770  aannenlem2  23888  aalioulem3  23893  taylf  23919  taylthlem2  23932  pserulm  23980  psercn2  23981  psercn  23984  reeff1olem  24004  efcvx  24007  loglesqrt  24299  rlimcnp  24492  xrlimcnp  24495  jensen  24515  wilthlem2  24595  vmadivsumb  24972  pntrsumo1  25054  pntlem3  25098  perpln2  25406  axcontlem10  25653  usgraexmplef  25929  nmoxr  27005  nmooge0  27006  nmoolb  27010  nmoubi  27011  ubthlem1  27110  shmodi  27633  nmopxr  28109  nmfnxr  28122  nmoplb  28150  nmopub  28151  nmfnlb  28167  nmfnleub  28168  nmopun  28257  branmfn  28348  mdslj1i  28562  hatomistici  28605  xppreima2  28830  fpwrelmap  28896  infxrge0gelb  28921  xrge0tsmsd  29116  metideq  29264  metider  29265  pstmfval  29267  esumgect  29479  esum2d  29482  sigaclci  29522  insiga  29527  omssubadd  29689  eulerpartlemgs2  29769  ballotlemsima  29904  signsply0  29954  bnj1145  30315  bnj1137  30317  bnj1136  30319  rescon  30482  cvmliftlem8  30528  cvmlift3lem6  30560  mclsssvlem  30713  mclsind  30721  mclsppslem  30734  nofulllem5  31105  ivthALT  31500  neibastop1  31524  topjoin  31530  ptrecube  32579  poimirlem6  32585  poimirlem15  32594  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  itg2gt0cn  32635  ftc1cnnc  32654  ftc1anclem3  32657  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirclem2  32671  areacirclem3  32672  areacirclem4  32673  totbndbnd  32758  prdsbnd  32762  heiborlem1  32780  rrnequiv  32804  reheibor  32808  iccbnd  32809  pmapssbaN  34064  2polssN  34219  paddunN  34231  poldmj1N  34232  ispsubcl2N  34251  psubclinN  34252  paddatclN  34253  poml4N  34257  diaglbN  35362  diaintclN  35365  dibglbN  35473  dibintclN  35474  dicssdvh  35493  dihvalrel  35586  dochexmidlem4  35770  rmxyelqirr  36493  ttac  36621  hbtlem6  36718  hbt  36719  itgpowd  36819  cnvssb  36911  cnvrcl0  36951  cnvtrrel  36981  relexpaddss  37029  cotrcltrcl  37036  cotrclrcl  37053  frege96d  37060  frege97d  37063  frege109d  37068  frege131d  37075  rp-imass  37085  rfovcnvf1od  37318  isotone2  37367  gneispace  37452  k0004ss1  37469  uzfissfz  38483  suplesup  38496  limciccioolb  38688  limcicciooub  38704  limcleqr  38711  cncfiooicclem1  38779  ibliccsinexp  38842  iblioosinexp  38844  itgcoscmulx  38861  itgsincmulx  38866  itgsubsticclem  38867  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem34  38927  stoweidlem59  38952  dirkeritg  38995  dirkercncflem2  38997  fourierdlem20  39020  fourierdlem31  39031  fourierdlem39  39039  fourierdlem42  39042  fourierdlem46  39045  fourierdlem52  39051  fourierdlem53  39052  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem68  39067  fourierdlem76  39075  fourierdlem85  39084  fourierdlem88  39087  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem93  39092  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fouriersw  39124  etransclem46  39173  etransclem48  39175  sge0less  39285  sge0resplit  39299  sge0isum  39320  pimdecfgtioo  39604  pimincfltioo  39605  iccpartipre  39959  bgoldbtbndlem2  40222  setrec1lem4  42236  setrec2fun  42238