Theorem syl5ss 3579

Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)

Hypotheses

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

Assertion

Ref	Expression
syl5ss	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl5ss

Step	Hyp	Ref	Expression
1		syl5ss.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3		syl5ss.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 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:  wereu2  5035  sofld  5500  fvmptss  6201  fimacnv  6255  isofr2  6494  frxp  7174  fnse  7181  smores2  7338  f1imaen2g  7903  domunsncan  7945  dffi3  8220  marypha1lem  8222  ordtypelem7  8312  ordtypelem8  8313  oismo  8328  unxpwdom2  8376  cantnfres  8457  oemapvali  8464  tskwe  8659  acndom2  8760  dfac2a  8835  dfac12lem2  8849  cfle  8959  cofsmo  8974  coftr  8978  isf34lem5  9083  isf34lem7  9084  isf34lem6  9085  enfin1ai  9089  fin1a2lem12  9116  ttukeylem7  9220  alephexp1  9280  fpwwe2lem13  9343  fpwwe2  9344  canth4  9348  canthwelem  9351  pwfseqlem1  9359  pwfseqlem4  9363  fzossnn0  12368  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  xptrrel  13567  limsupgle  14056  limsupgre  14060  rlimres  14137  lo1res  14138  lo1resb  14143  rlimresb  14144  o1resb  14145  o1of2  14191  o1rlimmul  14197  isercolllem2  14244  isercoll  14246  climsup  14248  fprodntriv  14511  bitsinvp1  15009  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  sadasslem  15030  sadeq  15032  bitsres  15033  smuval2  15042  smupval  15048  smueqlem  15050  smumul  15053  1arith  15469  isstruct2  15704  setscom  15731  ressress  15765  imasvscafn  16020  imasless  16023  mrcssv  16097  isacs1i  16141  mreacs  16142  acsfn  16143  isacs4lem  16991  isacs5lem  16992  mhmima  17186  cntzmhm  17594  f1omvdconj  17689  f1omvdco2  17691  symgsssg  17710  symggen  17713  psgnunilem1  17736  efgval  17953  gsumzaddlem  18144  gsumconst  18157  dmdprdd  18221  dprdfeq0  18244  dprdres  18250  dprdss  18251  dprdz  18252  subgdmdprd  18256  dprddisj2  18261  dprd2dlem1  18263  dprd2da  18264  dprd2d2  18266  dmdprdsplit2lem  18267  lmhmlsp  18870  lsppratlem4  18971  islbs3  18976  lbsextlem3  18981  mplcoe5  19289  mplind  19323  znleval  19722  evpmss  19751  frlmsslsp  19954  lindff1  19978  lindfrn  19979  f1lindf  19980  lindfmm  19985  lsslindf  19988  basdif0  20568  tgcl  20584  ppttop  20621  epttop  20623  ntrin  20675  mretopd  20706  neiptoptop  20745  cnclsi  20886  cnconst2  20897  cnrest2  20900  cnpresti  20902  cnprest2  20904  fiuncmp  21017  connsub  21034  conima  21038  iunconlem  21040  1stcfb  21058  2ndc1stc  21064  2ndcdisj  21069  kgentopon  21151  llycmpkgen2  21163  1stckgenlem  21166  kgencn3  21171  ptclsg  21228  ptcnplem  21234  txtube  21253  hausdiag  21258  txkgen  21265  xkoco1cn  21270  xkoco2cn  21271  xkococnlem  21272  qtoptop2  21312  basqtop  21324  imastopn  21333  hmeores  21384  hmphdis  21409  ptcmpfi  21426  fbssfi  21451  filin  21468  infil  21477  fbasrn  21498  fgtr  21504  elfm  21561  imaelfm  21565  hausflim  21595  flimclslem  21598  fclscmp  21644  cnextcn  21681  tmdgsum2  21710  tgpconcomp  21726  ustexsym  21829  ustund  21835  ustimasn  21842  utoptop  21848  utopbas  21849  restutopopn  21852  blin2  22044  metustexhalf  22171  icccmplem2  22434  icccmplem3  22435  reconnlem2  22438  tchcph  22844  fmcfil  22878  resscdrg  22962  ivthlem2  23028  ivthlem3  23029  ivth2  23031  ovolfiniun  23076  ovoliunlem1  23077  ismbl2  23102  nulmbl2  23111  unmbl  23112  shftmbl  23113  voliunlem1  23125  voliunlem2  23126  ioombl1lem4  23136  uniioombllem4  23160  dyadmbllem  23173  dyadmbl  23174  mbflimsup  23239  i1fima  23251  i1fima2  23252  i1fadd  23268  itg1addlem4  23272  itg2splitlem  23321  itg2split  23322  ellimc3  23449  limcflflem  23450  limcflf  23451  limcresi  23455  limciun  23464  dvreslem  23479  dvres2lem  23480  dvres  23481  dvaddbr  23507  dvmulbr  23508  dvlip  23560  dvlip2  23562  c1liplem1  23563  dvivthlem1  23575  dvne0  23578  lhop1lem  23580  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvfsumle  23588  dvfsumabs  23590  dvfsumlem2  23594  itgsubstlem  23615  mdegleb  23628  mdeglt  23629  mdegldg  23630  mdegxrcl  23631  mdegcl  23633  ig1peu  23735  reeff1olem  24004  logccv  24209  rlimcnp2  24493  lgamgulmlem2  24556  ppisval  24630  prmdvdsfi  24633  mumul  24707  sqff1o  24708  chtlepsi  24731  chpub  24745  dchrisum0lem2a  25006  pntlem3  25098  ex-res  26690  htthlem  27158  chlejb1i  27719  ssmd2  28555  fimarab  28825  gsumle  29110  locfinreflem  29235  sibfof  29729  sitgclbn  29732  sitgaddlemb  29737  eulerpartlemgu  29766  ballotlemsima  29904  bnj1311  30346  erdsze2lem2  30440  iccllyscon  30486  cvmopnlem  30514  msrf  30693  nodenselem6  31085  nofulllem5  31105  neiin  31497  neibastop1  31524  neibastop2lem  31525  topmeet  31529  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem19  32598  poimirlem30  32609  cnambfre  32628  itg2gt0cn  32635  sstotbnd2  32743  sstotbnd3  32745  ssbnd  32757  ismtyima  32772  heibor1lem  32778  pmodlem2  34151  pmodN  34154  diaintclN  35365  djaclN  35443  dibintclN  35474  dicval  35483  dihoml4c  35683  djhcl  35707  isnacs2  36287  isnacs3  36291  diophrw  36340  pellfundre  36463  pellfundge  36464  pellfundlb  36466  pellfundglb  36467  fnwe2lem2  36639  lmhmfgima  36672  hbt  36719  cnvtrcl0  36952  trclrelexplem  37022  relexp0a  37027  rp-imass  37085  isotone2  37367  climinf  38673  islptre  38686  limccog  38687  limcleqr  38711  itgcoscmulx  38861  ismbl3  38879  ismbl4  38886  stoweidlem27  38920  dirkercncflem2  38997  fourierdlem38  39038  fourierdlem49  39048  fourierdlem51  39050  fourierdlem54  39053  fourierdlem63  39062  fourierdlem68  39067  fourierdlem69  39068  fourierdlem70  39069  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem80  39079  fourierdlem84  39083  fourierdlem85  39084  fourierdlem88  39087  fourierdlem100  39099  fourierdlem101  39100  fourierdlem104  39103  fourierdlem107  39106  fourierdlem111  39110  fourierdlem112  39111  caragenel2d  39422  hoidmv1lelem3  39483  hspmbllem3  39518  sssmf  39625  smfrec  39674  av-extwwlkfablem2  41510  mgmhmima  41592