Theorem sstrd 3946

Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)

Hypotheses

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

Assertion

Ref	Expression
sstrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sstrd

Step	Hyp	Ref	Expression
1		sstrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sstrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		sstr 3944	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3921

This theorem is referenced by:  sstrid  3947  sstrdi  3948  rabssrabd  4036  ssdif2d  4101  uniintsn  4942  funss  6536  fssxp  6715  knatar  7337  tfisi  7835  suppssov1  8172  suppssov2  8173  suppssfv  8177  tposss  8202  frrlem8  8269  tfrlem1  8341  omwordri  8536  oewordri  8557  oeeui  8567  oaabs2  8614  omopthlem1  8624  ecinxp  8769  sbthlem1  9055  dffi2  9366  hartogslem1  9487  cantnfcl  9619  cantnflt  9624  cantnfp1lem3  9632  cantnflem3  9643  cnfcom  9652  cnfcom3lem  9655  ttrcltr  9668  rankssb  9803  tskwe  9905  dfac12lem2  10098  dfac12lem3  10099  cfflb  10213  cfcof  10228  ssfin2  10274  hsmexlem4  10383  ttukeylem6  10468  ttukeylem7  10469  fpwwe2lem1  10586  fpwwe2lem7  10592  fpwwe2lem10  10595  fpwwe2lem11  10596  canthnumlem  10603  canthwelem  10605  canthwe  10606  canthp1lem2  10608  pwfseqlem5  10618  wunex2  10693  tsktrss  10716  inttsk  10729  uzwo3  12941  xrsupssd  13333  supicc  13502  supiccub  13503  supicclub  13504  ssfzunsnext  13571  seqsplit  14045  seqf1olem2a  14050  seqz  14060  swrdval2  14657  trrelssd  14983  rtrclreclem4  15071  sumss  15734  qshash  15838  incexc  15850  incexc2  15851  prodss  15960  rpnnen2lem11  16239  vdwlem1  17000  ramub1lem1  17045  imasaddvallem  17542  imasvscaf  17552  mrerintcl  17608  ismred2  17614  mremre  17615  mrcuni  17636  mressmrcd  17642  submrc  17643  mrissmrid  17656  mreexexlem2d  17660  isacs2  17668  isacs1i  17672  invss  17777  ssctr  17841  funcres2b  17913  isacs3lem  18557  acsfiindd  18568  acsmapd  18569  acsmap2d  18570  tsrdir  18619  subsubmgm  18727  subsubm  18833  gsumwspan  18863  subsubg  19174  subgint  19175  cntzidss  19363  symggen  19493  pmtrdifellem1  19499  pmtrdifellem2  19500  pgpssslw  19637  lsmless1x  19667  lsmless2x  19668  lsmless12  19685  subglsm  19696  gsumval3lem2  19929  gsumzaddlem  19944  gsumzadd  19945  gsum2d  19995  dmdprdd  20024  dprdfeq0  20047  dprdspan  20052  dprdres  20053  dprdss  20054  dprdz  20055  subgdmdprd  20059  subgdprd  20060  dprdsn  20061  dprd2dlem1  20066  dprd2da  20067  dmdprdsplit2lem  20070  dprdsplit  20073  pgpfac1lem2  20100  pgpfac1lem3  20102  pgpfac1lem5  20104  subsubrng  20592  subsubrg  20627  subdrgint  20832  lspss  21031  lspun  21034  lsslsp  21062  lmhmlsp  21096  lsmelval2  21132  lsmssspx  21135  lsppratlem2  21198  lsppratlem3  21199  lsppratlem4  21200  lbsextlem2  21209  lbsextlem3  21210  ocvlsp  21708  cssmre  21725  obselocv  21760  obslbs  21762  aspss  21908  mhpaddcl  22196  mhpinvcl  22197  mhpvscacl  22199  psdmullem  22210  toponmre  23133  neiint  23144  neiss  23149  lpss  23182  lpss3  23184  restopnb  23215  restfpw  23219  neitr  23220  restcls  23221  restntr  23222  restlp  23223  ordtbas  23232  pnfnei  23260  mnfnei  23261  iscnp4  23303  cnclsi  23312  isreg2  23417  discmp  23438  cmpcld  23442  uncmp  23443  sscmp  23445  hauscmplem  23446  cmpfi  23448  iunconnlem  23467  clsconn  23470  2ndcctbss  23495  restnlly  23522  llyrest  23525  nllyrest  23526  llyidm  23528  nllyidm  23529  cldllycmp  23535  dislly  23537  comppfsc  23572  llycmpkgen2  23590  ptbasfi  23621  txnlly  23677  txcmplem1  23681  tx1stc  23690  xkococnlem  23699  qtopval2  23736  basqtop  23751  tgqtop  23752  qtoprest  23757  kqreglem1  23781  kqreglem2  23782  kqnrmlem1  23783  kqnrmlem2  23784  fsubbas  23907  fgabs  23919  fbasrn  23924  trfil2  23927  trfg  23931  isufil2  23948  trufil  23950  ssufl  23958  ufileu  23959  filufint  23960  fmfnfmlem4  23997  fmfnfm  23998  flimss2  24012  flimss1  24013  fclsfnflim  24067  flimfnfcls  24068  fclscmp  24070  cnpfcfi  24080  alexsubALT  24091  clssubg  24149  clsnsg  24150  tsmsres  24184  ustexsym  24256  ustex2sym  24257  ustex3sym  24258  ustneism  24264  trust  24269  utoptop  24274  restutopopn  24278  utop2nei  24290  utopreg  24292  cfiluweak  24334  neipcfilu  24335  blssps  24464  blss  24465  blcld  24545  blsscls  24547  met1stc  24561  met2ndci  24562  metust  24598  cfilucfil  24599  restmetu  24610  tgqioo  24840  xrsblre  24852  reconnlem2  24868  xrge0gsumle  24874  xrge0tsms  24875  rescncf  24939  cnmpopc  24970  cnheibor  24997  cnllycmp  24998  lebnum  25006  phtpycn  25025  cfilfcls  25316  iscmet3lem2  25334  cmetss  25358  cncmet  25364  bcthlem4  25369  bcth3  25373  rrxcph  25434  rrxmetlem  25449  minveclem4a  25472  minveclem4  25474  ivthicc  25500  ovollb  25521  ovollb2lem  25530  ovollb2  25531  nulmbl2  25578  ioorcl2  25614  uniioombllem3  25627  uniioombllem4  25628  uniioombllem5  25629  opnmbllem  25643  volcn  25648  volivth  25649  mbfeqalem1  25683  itg10a  25752  mbfi1fseqlem4  25760  ditgcl  25900  ditgswap  25901  ditgsplitlem  25902  limcflf  25923  limcres  25928  dvbss  25943  dvbsss  25944  perfdvf  25945  dvreslem  25951  dvres2lem  25952  dvres3  25955  dvmptresicc  25958  dvcnp  25961  dvcnp2  25962  dvcn  25963  dvnff  25965  dvn2bss  25972  dvnres  25973  cpnord  25977  dvaddbr  25980  dvmulbr  25981  dvcobr  25988  dvnfre  25994  dvmptres2  26004  dvmptntr  26013  dvcnvlem  26018  dvcnv  26019  dvferm1lem  26026  dvferm2lem  26028  dvlip  26035  dvlipcn  26036  dvlip2  26037  c1liplem1  26038  dvgt0lem1  26044  lhop1lem  26055  lhop  26058  dvcnvrelem1  26059  dvcnvrelem2  26060  dvcnvre  26061  dvfsumle  26063  dvfsumge  26064  dvfsumabs  26065  ftc1lem1  26077  ftc1lem2  26078  ftc1a  26079  ftc1lem4  26081  ftc2ditglem  26087  itgsubstlem  26090  ig1peu  26215  ig1pdvds  26220  taylfvallem1  26397  tayl0  26402  taylply2  26408  taylply  26409  dvtaylp  26410  dvntaylp  26411  dvntaylp0  26412  taylthlem1  26413  ulmdvlem1  26440  ulmdvlem3  26442  psercn  26466  pserdvlem2  26468  abelth  26481  xrlimcnp  27010  lgamucov  27079  wilthlem2  27110  sqff1o  27223  chtublem  27252  pntlemq  27642  pntlemf  27646  ssslts1  27843  ssslts2  27844  cutbdaybnd  27865  cutbdaybnd2  27866  eqcuts3  27874  cofss  28000  coiniss  28001  bdaypw2bnd  28535  bdayfinbndlem1  28537  z12bdaylem2  28541  tglineintmo  28788  ttgcontlem1  29031  pthdlem1  29912  shintcli  31478  shub1  31531  mdslmd1lem1  32474  mdexchi  32484  chirredlem1  32539  mdsymlem5  32556  sumdmdii  32564  sumdmdlem2  32568  fnpreimac  32822  fsuppinisegfi  32839  xrge0infssd  32913  swrdrn3  33094  swrdf1  33095  swrdrndisj  33096  pwrssmgc  33139  xrge0tsmsd  33214  elrgspnlem4  33387  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  fldgenss  33464  fldgenssp  33466  linds2eq  33528  elrspunidl  33575  ssdifidllem  33604  ssdifidlprm  33606  mxidlprm  33619  ssmxidllem  33622  ssmxidl  33623  qsdrnglem2  33645  rprmdvdsprod  33691  ressply1evls1  33722  resssra  33845  lsssra  33846  exsslsb  33855  lbsdiflsp0  33884  dimkerim  33885  fedgmullem1  33887  fedgmullem2  33888  fedgmul  33889  dimlssid  33890  fldextrspunlsplem  33931  fldextrspunlsp  33932  fldextrspunlem1  33933  fldextrspundgdvdslem  33938  fldextrspundgdvds  33939  constr01  34000  constrmon  34002  constrextdg2lem  34006  constrfiss  34009  smatrcl  34054  locfinreflem  34098  cmpcref  34108  zarclsun  34128  zarclsiin  34129  zarclssn  34131  zarcmplem  34139  pnfneige0  34209  esum2d  34351  insiga  34395  sssigagen2  34404  dynkin  34425  dya2iocnei  34540  omsmon  34556  carsgclctunlem1  34575  carsggect  34576  omsmeas  34581  ftc2re  34856  fdvneggt  34858  fdvnegge  34860  reprsuc  34873  reprss  34875  reprlt  34877  reprinfz1  34880  logdivsqrle  34908  hgt750lemb  34914  bnj906  35189  bnj1020  35224  bnj1137  35254  bnj1408  35295  bnj1452  35311  rankval4b  35360  fineqvnttrclselem2  35382  erdszelem7  35511  erdszelem8  35512  erdsze2lem1  35517  connpconn  35549  cvmliftmolem1  35595  cvmlift2lem1  35616  cvmlift2lem9  35625  cvmlift2lem10  35626  cvmlift3lem6  35638  cvmlift3lem7  35639  satfsschain  35678  ss2mcls  35882  neibastop2lem  36684  fnemeet2  36691  fnejoin1  36692  ontgval  36755  ttcmin  36820  unbdqndv1  36910  opnmbllem0  38119  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  sstotbnd2  38237  heiborlem1  38274  heiborlem8  38281  intidl  38492  lsmsat  39596  lssats  39600  lpssat  39601  lssatle  39603  lssat  39604  lsatcvatlem  39637  paddss12  40407  paddasslem17  40424  pmodlem1  40434  pmod1i  40436  pmodl42N  40439  elpcliN  40481  pclfinN  40488  polcon3N  40505  polcon2N  40507  paddunN  40515  pclfinclN  40538  poml5N  40542  osumcllem1N  40544  osumcllem2N  40545  osumcllem3N  40546  pl42lem2N  40568  pl42lem4N  40570  cdlemn5pre  41788  dihord1  41806  dihord2a  41807  dihord2b  41808  dihord5b  41847  dochss  41953  dochdmj1  41978  djhsumss  41995  djhunssN  41997  dochexmidlem2  42049  lclkrslem1  42125  lclkrslem2  42126  lcfrlem2  42131  aks4d1p4  42660  aks4d1p5  42661  aks4d1p7  42664  aks4d1p8  42668  aks6d1c2  42711  sticksstones1  42727  unitscyglem5  42780  prjcrv0  43179  elrfi  43239  ismrcd1  43243  istopclsd  43245  mrefg2  43252  aomclem2  43596  aomclem6  43600  hbtlem6  43670  hbt  43671  oege2  43848  cantnftermord  43861  omabs2  43873  tfsconcat0b  43887  naddgeoa  43935  naddwordnexlem0  43937  naddwordnexlem1  43938  dfno2  43968  mptrcllem  44153  dfrcl2  44214  relexp0a  44256  trclimalb2  44266  frege81d  44287  k0004ss2  44692  imo72b2lem2  44707  imo72b2  44712  uzwo4  45597  ssin0  45599  ixpssmapc  45617  ssinc  45629  ssdec  45630  supxrre3  45865  uzfissfz  45866  ssuzfz  45889  supminfxr  46002  inficc  46074  ressiocsup  46094  ressioosup  46095  ressiooinf  46097  limccog  46160  limclner  46189  limsupres  46243  limsupresuz2  46247  limsupequzlem  46260  supcnvlimsup  46278  limsupgtlem  46315  liminfresuz2  46325  cncfmptssg  46409  icccncfext  46425  dvresntr  46456  dvbdfbdioolem1  46466  dvdmsscn  46474  dvnxpaek  46480  dvnprodlem2  46485  stoweidlem59  46597  fourierdlem20  46665  fourierdlem42  46687  fourierdlem48  46692  fourierdlem49  46693  fourierdlem52  46696  fourierdlem58  46702  fourierdlem64  46708  fourierdlem73  46717  fourierdlem76  46720  fourierdlem80  46724  fourierdlem84  46728  fourierdlem93  46737  fourierdlem103  46747  fourierdlem104  46748  fourierdlem113  46757  etransclem18  46790  ioorrnopnlem  46842  salincl  46862  intsal  46868  fsumlesge0  46915  sge0cl  46919  sge0supre  46927  sge0less  46930  sge0split  46947  sge0seq  46984  caragensspw  47047  omessre  47048  caragendifcl  47052  caratheodorylem1  47064  0ome  47067  omess0  47072  caragencmpl  47073  hoissrrn  47087  hoicvrrex  47094  ovnlecvr  47096  ovnsslelem  47098  ovnssle  47099  ovnsubaddlem1  47108  hoissrrn2  47116  hoidmv1lelem1  47129  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem4  47136  ovnlecvr2  47148  voncmpl  47159  hspmbl  47167  opnvonmbllem1  47170  ovolval5lem2  47191  ovolval5lem3  47192  vonioolem1  47218  pimdecfgtioc  47253  pimincfltioc  47254  pimdecfgtioo  47255  pimincfltioo  47256  issmflem  47265  cnfsmf  47278  incsmflem  47279  smfsssmf  47281  smfadd  47303  decsmflem  47304  smflim  47315  smfres  47328  smfmul  47333  smfpimbor1lem1  47336  smfco  47340  smfsuplem1  47349  smfsuplem3  47351  smflimsuplem1  47358  smflimsuplem4  47361  smflimsuplem7  47364  nndivides2  47942  cnneiima  49502  seposep  49511  iscnrm3rlem4  49528  iscnrm3llem1  49534  lubsscl  49545  glbsscl  49546  toplatglb  49586  setrecsss  50286  elpglem1  50296