Theorem sstrd 3948

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 3946	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3906

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3923

This theorem is referenced by:  sstrid  3949  sstrdi  3950  rabssrabd  4038  ssdif2d  4103  uniintsn  4951  funss  6557  fssxp  6735  knatar  7357  tfisi  7856  suppssov1  8194  suppssov2  8195  suppssfv  8199  tposss  8224  frrlem8  8291  tfrlem1  8363  omwordri  8558  oewordri  8579  oeeui  8589  oaabs2  8636  omopthlem1  8646  ecinxp  8791  sbthlem1  9076  dffi2  9384  hartogslem1  9505  cantnfcl  9637  cantnflt  9642  cantnfp1lem3  9650  cantnflem3  9661  cnfcom  9670  cnfcom3lem  9673  ttrcltr  9686  rankssb  9821  tskwe  9937  dfac12lem2  10129  dfac12lem3  10130  cfflb  10244  cfcof  10259  ssfin2  10305  hsmexlem4  10414  ttukeylem6  10499  ttukeylem7  10500  fpwwe2lem1  10617  fpwwe2lem7  10623  fpwwe2lem10  10626  fpwwe2lem11  10627  canthnumlem  10634  canthwelem  10636  canthwe  10637  canthp1lem2  10639  pwfseqlem5  10649  wunex2  10724  tsktrss  10747  inttsk  10760  uzwo3  12968  xrsupssd  13360  supicc  13529  supiccub  13530  supicclub  13531  ssfzunsnext  13599  seqsplit  14073  seqf1olem2a  14078  seqz  14088  swrdval2  14686  trrelssd  15012  rtrclreclem4  15100  sumss  15777  qshash  15881  incexc  15893  incexc2  15894  prodss  16003  rpnnen2lem11  16281  vdwlem1  17042  ramub1lem1  17087  imasaddvallem  17584  imasvscaf  17594  mrerintcl  17650  ismred2  17656  mremre  17657  mrcuni  17678  mressmrcd  17684  submrc  17685  mrissmrid  17698  mreexexlem2d  17702  isacs2  17710  isacs1i  17714  invss  17819  ssctr  17883  funcres2b  17955  isacs3lem  18599  acsfiindd  18610  acsmapd  18611  acsmap2d  18612  tsrdir  18661  subsubmgm  18769  subsubm  18876  gsumwspan  18906  subsubg  19217  subgint  19218  cntzidss  19411  symggen  19541  pmtrdifellem1  19547  pmtrdifellem2  19548  pgpssslw  19685  lsmless1x  19715  lsmless2x  19716  lsmless12  19733  subglsm  19744  gsumval3lem2  19977  gsumzaddlem  19992  gsumzadd  19993  gsum2d  20043  dmdprdd  20072  dprdfeq0  20095  dprdspan  20100  dprdres  20101  dprdss  20102  dprdz  20103  subgdmdprd  20107  subgdprd  20108  dprdsn  20109  dprd2dlem1  20114  dprd2da  20115  dmdprdsplit2lem  20118  dprdsplit  20121  pgpfac1lem2  20148  pgpfac1lem3  20150  pgpfac1lem5  20152  subsubrng  20649  subsubrg  20684  subdrgint  20887  lspss  21086  lspun  21089  lsslsp  21117  lmhmlsp  21151  lsmelval2  21187  lsmssspx  21190  lsppratlem2  21253  lsppratlem3  21254  lsppratlem4  21255  lbsextlem2  21264  lbsextlem3  21265  ssdifidllem  21465  ssdifidlprm  21467  ocvlsp  21807  cssmre  21824  obselocv  21859  obslbs  21861  aspss  22007  mhpaddcl  22295  mhpinvcl  22296  mhpvscacl  22298  psdmullem  22309  toponmre  23231  neiint  23242  neiss  23247  lpss  23280  lpss3  23282  restopnb  23313  restfpw  23317  neitr  23318  restcls  23319  restntr  23320  restlp  23321  ordtbas  23330  pnfnei  23358  mnfnei  23359  iscnp4  23401  cnclsi  23410  isreg2  23515  discmp  23536  cmpcld  23540  uncmp  23541  sscmp  23543  hauscmplem  23544  cmpfi  23546  iunconnlem  23565  clsconn  23568  2ndcctbss  23593  restnlly  23620  llyrest  23623  nllyrest  23624  llyidm  23626  nllyidm  23627  cldllycmp  23633  dislly  23635  comppfsc  23670  llycmpkgen2  23688  ptbasfi  23719  txnlly  23775  txcmplem1  23779  tx1stc  23788  xkococnlem  23797  qtopval2  23834  basqtop  23849  tgqtop  23850  qtoprest  23855  kqreglem1  23879  kqreglem2  23880  kqnrmlem1  23881  kqnrmlem2  23882  fsubbas  24005  fgabs  24017  fbasrn  24022  trfil2  24025  trfg  24029  isufil2  24046  trufil  24048  ssufl  24056  ufileu  24057  filufint  24058  fmfnfmlem4  24095  fmfnfm  24096  flimss2  24110  flimss1  24111  fclsfnflim  24165  flimfnfcls  24166  fclscmp  24168  cnpfcfi  24178  alexsubALT  24189  clssubg  24247  clsnsg  24248  tsmsres  24282  ustexsym  24354  ustex2sym  24355  ustex3sym  24356  ustneism  24362  trust  24367  utoptop  24372  restutopopn  24376  utop2nei  24388  utopreg  24390  cfiluweak  24432  neipcfilu  24433  blssps  24562  blss  24563  blcld  24643  blsscls  24645  met1stc  24659  met2ndci  24660  metust  24696  cfilucfil  24697  restmetu  24708  tgqioo  24938  xrsblre  24950  reconnlem2  24966  xrge0gsumle  24972  xrge0tsms  24973  rescncf  25037  cnmpopc  25068  cnheibor  25095  cnllycmp  25096  lebnum  25104  phtpycn  25123  cfilfcls  25414  iscmet3lem2  25432  cmetss  25456  cncmet  25462  bcthlem4  25467  bcth3  25471  rrxcph  25532  rrxmetlem  25547  minveclem4a  25570  minveclem4  25572  ivthicc  25598  ovollb  25619  ovollb2lem  25628  ovollb2  25629  nulmbl2  25676  ioorcl2  25712  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  opnmbllem  25741  volcn  25746  volivth  25747  mbfeqalem1  25781  itg10a  25850  mbfi1fseqlem4  25858  ditgcl  25998  ditgswap  25999  ditgsplitlem  26000  limcflf  26021  limcres  26026  dvbss  26041  dvbsss  26042  perfdvf  26043  dvreslem  26049  dvres2lem  26050  dvres3  26053  dvmptresicc  26056  dvcnp  26059  dvcnp2  26060  dvcn  26061  dvnff  26063  dvn2bss  26070  dvnres  26071  cpnord  26075  dvaddbr  26078  dvmulbr  26079  dvcobr  26086  dvnfre  26092  dvmptres2  26102  dvmptntr  26111  dvcnvlem  26116  dvcnv  26117  dvferm1lem  26124  dvferm2lem  26126  dvlip  26133  dvlipcn  26134  dvlip2  26135  c1liplem1  26136  dvgt0lem1  26142  lhop1lem  26153  lhop  26156  dvcnvrelem1  26157  dvcnvrelem2  26158  dvcnvre  26159  dvfsumle  26161  dvfsumge  26162  dvfsumabs  26163  ftc1lem1  26175  ftc1lem2  26176  ftc1a  26177  ftc1lem4  26179  ftc2ditglem  26185  itgsubstlem  26188  ig1peu  26313  ig1pdvds  26318  taylfvallem1  26498  tayl0  26503  taylply2  26509  taylply  26510  dvtaylp  26511  dvntaylp  26512  dvntaylp0  26513  taylthlem1  26514  ulmdvlem1  26541  ulmdvlem3  26543  psercn  26567  pserdvlem2  26569  abelth  26582  xrlimcnp  27111  lgamucov  27180  wilthlem2  27211  sqff1o  27324  chtublem  27353  pntlemq  27743  pntlemf  27747  ssslts1  27944  ssslts2  27945  cutbdaybnd  27966  cutbdaybnd2  27967  eqcuts3  27975  cofss  28101  coiniss  28102  bdaypw2bnd  28636  bdayfinbndlem1  28638  z12bdaylem2  28642  tglineintmo  28893  ttgcontlem1  29212  pthdlem1  30093  shintcli  31659  shub1  31712  mdslmd1lem1  32655  mdexchi  32665  chirredlem1  32720  mdsymlem5  32737  sumdmdii  32745  sumdmdlem2  32749  fnpreimac  32993  fsuppinisegfi  33010  xrge0infssd  33084  swrdrn3  33253  swrdf1  33254  swrdrndisj  33255  pwrssmgc  33298  xrge0tsmsd  33371  elrgspnlem4  33543  elrgspnsubrunlem1  33545  elrgspnsubrunlem2  33546  fldgenss  33615  fldgenssp  33617  linds2eq  33672  elrspunidl  33714  mxidlprm  33731  ssmxidllem  33734  ssmxidl  33735  qsdrnglem2  33756  rprmdvdsprod  33802  ressply1evls1  33833  resssra  33955  lsssra  33956  exsslsb  33965  lbsdiflsp0  33994  dimkerim  33995  fedgmullem1  33997  fedgmullem2  33998  fedgmul  33999  dimlssid  34000  fldextrspunlsplem  34041  fldextrspunlsp  34042  fldextrspunlem1  34043  fldextrspundgdvdslem  34048  fldextrspundgdvds  34049  constr01  34110  constrmon  34112  constrextdg2lem  34116  constrfiss  34119  smatrcl  34164  locfinreflem  34208  cmpcref  34218  zarclsun  34238  zarclsiin  34239  zarclssn  34241  zarcmplem  34249  pnfneige0  34319  esum2d  34461  insiga  34505  sssigagen2  34514  dynkin  34535  dya2iocnei  34650  omsmon  34666  carsgclctunlem1  34685  carsggect  34686  omsmeas  34691  ftc2re  34963  fdvneggt  34965  fdvnegge  34967  reprsuc  34980  reprss  34982  reprlt  34984  reprinfz1  34987  logdivsqrle  35015  hgt750lemb  35021  bnj906  35296  bnj1020  35331  bnj1137  35361  bnj1408  35402  bnj1452  35418  rankval4b  35471  fineqvnttrclselem2  35513  erdszelem7  35667  erdszelem8  35668  erdsze2lem1  35673  connpconn  35705  cvmliftmolem1  35751  cvmlift2lem1  35772  cvmlift2lem9  35781  cvmlift2lem10  35782  cvmlift3lem6  35794  cvmlift3lem7  35795  satfsschain  35834  ss2mcls  36038  neibastop2lem  36849  fnemeet2  36856  fnejoin1  36857  ontgval  36920  ttcmin  36985  unbdqndv1  37075  opnmbllem0  38285  ftc1anclem7  38328  ftc1anclem8  38329  ftc1anc  38330  sstotbnd2  38403  heiborlem1  38440  heiborlem8  38447  intidl  38658  lsmsat  39760  lssats  39764  lpssat  39765  lssatle  39767  lssat  39768  lsatcvatlem  39801  paddss12  40571  paddasslem17  40588  pmodlem1  40598  pmod1i  40600  pmodl42N  40603  elpcliN  40645  pclfinN  40652  polcon3N  40669  polcon2N  40671  paddunN  40679  pclfinclN  40702  poml5N  40706  osumcllem1N  40708  osumcllem2N  40709  osumcllem3N  40710  pl42lem2N  40732  pl42lem4N  40734  cdlemn5pre  41952  dihord1  41970  dihord2a  41971  dihord2b  41972  dihord5b  42011  dochss  42117  dochdmj1  42142  djhsumss  42159  djhunssN  42161  dochexmidlem2  42213  lclkrslem1  42289  lclkrslem2  42290  lcfrlem2  42295  aks4d1p4  42824  aks4d1p5  42825  aks4d1p7  42828  aks4d1p8  42832  aks6d1c2  42875  sticksstones1  42891  unitscyglem5  42944  prjcrv0  43345  elrfi  43405  ismrcd1  43409  istopclsd  43411  mrefg2  43418  aomclem2  43762  aomclem6  43766  hbtlem6  43836  hbt  43837  oege2  44014  cantnftermord  44027  omabs2  44039  tfsconcat0b  44053  naddgeoa  44101  naddwordnexlem0  44103  naddwordnexlem1  44104  dfno2  44134  mptrcllem  44319  dfrcl2  44380  relexp0a  44422  trclimalb2  44432  frege81d  44453  k0004ss2  44858  imo72b2lem2  44873  imo72b2  44878  uzwo4  45753  ssin0  45755  ixpssmapc  45773  ssinc  45785  ssdec  45786  supxrre3  46021  uzfissfz  46022  ssuzfz  46045  supminfxr  46158  inficc  46230  ressiocsup  46250  ressioosup  46251  ressiooinf  46253  limccog  46316  limclner  46345  limsupres  46399  limsupresuz2  46403  limsupequzlem  46416  supcnvlimsup  46434  limsupgtlem  46471  liminfresuz2  46481  cncfmptssg  46565  icccncfext  46581  dvresntr  46612  dvbdfbdioolem1  46622  dvdmsscn  46630  dvnxpaek  46636  dvnprodlem2  46641  stoweidlem59  46753  fourierdlem20  46821  fourierdlem42  46843  fourierdlem48  46848  fourierdlem49  46849  fourierdlem52  46852  fourierdlem58  46858  fourierdlem64  46864  fourierdlem73  46873  fourierdlem76  46876  fourierdlem80  46880  fourierdlem84  46884  fourierdlem93  46893  fourierdlem103  46903  fourierdlem104  46904  fourierdlem113  46913  etransclem18  46946  ioorrnopnlem  46998  salincl  47018  intsal  47024  fsumlesge0  47071  sge0cl  47075  sge0supre  47083  sge0less  47086  sge0split  47103  sge0seq  47140  caragensspw  47203  omessre  47204  caragendifcl  47208  caratheodorylem1  47220  0ome  47223  omess0  47228  caragencmpl  47229  hoissrrn  47243  hoicvrrex  47250  ovnlecvr  47252  ovnsslelem  47254  ovnssle  47255  ovnsubaddlem1  47264  hoissrrn2  47272  hoidmv1lelem1  47285  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem4  47292  ovnlecvr2  47304  voncmpl  47315  hspmbl  47323  opnvonmbllem1  47326  ovolval5lem2  47347  ovolval5lem3  47348  vonioolem1  47374  pimdecfgtioc  47409  pimincfltioc  47410  pimdecfgtioo  47411  pimincfltioo  47412  issmflem  47421  cnfsmf  47434  incsmflem  47435  smfsssmf  47437  smfadd  47459  decsmflem  47460  smflim  47471  smfres  47484  smfmul  47489  smfpimbor1lem1  47492  smfco  47496  smfsuplem1  47505  smfsuplem3  47507  smflimsuplem1  47514  smflimsuplem4  47517  smflimsuplem7  47520  nndivides2  48098  cnneiima  49672  seposep  49681  iscnrm3rlem4  49698  iscnrm3llem1  49704  lubsscl  49715  glbsscl  49716  toplatglb  49756  setrecsss  50456  elpglem1  50466