Theorem sstrd 3933

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

Syntax hints:   → wi 4   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3907

This theorem is referenced by:  sstrid  3934  sstrdi  3935  rabssrabd  4024  ssdif2d  4089  uniintsn  4928  funss  6511  fssxp  6689  knatar  7305  tfisi  7803  suppssov1  8140  suppssov2  8141  suppssfv  8145  tposss  8170  frrlem8  8236  tfrlem1  8308  omwordri  8500  oewordri  8521  oeeui  8531  oaabs2  8578  omopthlem1  8588  ecinxp  8732  sbthlem1  9018  dffi2  9329  hartogslem1  9450  cantnfcl  9579  cantnflt  9584  cantnfp1lem3  9592  cantnflem3  9603  cnfcom  9612  cnfcom3lem  9615  ttrcltr  9628  rankssb  9763  tskwe  9865  dfac12lem2  10058  dfac12lem3  10059  cfflb  10172  cfcof  10187  ssfin2  10233  hsmexlem4  10342  ttukeylem6  10427  ttukeylem7  10428  fpwwe2lem1  10545  fpwwe2lem7  10551  fpwwe2lem10  10554  fpwwe2lem11  10555  canthnumlem  10562  canthwelem  10564  canthwe  10565  canthp1lem2  10567  pwfseqlem5  10577  wunex2  10652  tsktrss  10675  inttsk  10688  uzwo3  12884  xrsupssd  13276  supicc  13445  supiccub  13446  supicclub  13447  ssfzunsnext  13514  seqsplit  13988  seqf1olem2a  13993  seqz  14003  swrdval2  14600  trrelssd  14926  rtrclreclem4  15014  sumss  15677  qshash  15781  incexc  15793  incexc2  15794  prodss  15903  rpnnen2lem11  16182  vdwlem1  16943  ramub1lem1  16988  imasaddvallem  17484  imasvscaf  17494  mrerintcl  17550  ismred2  17556  mremre  17557  mrcuni  17578  mressmrcd  17584  submrc  17585  mrissmrid  17598  mreexexlem2d  17602  isacs2  17610  isacs1i  17614  invss  17719  ssctr  17783  funcres2b  17855  isacs3lem  18499  acsfiindd  18510  acsmapd  18511  acsmap2d  18512  tsrdir  18561  subsubmgm  18669  subsubm  18775  gsumwspan  18805  subsubg  19116  subgint  19117  cntzidss  19306  symggen  19436  pmtrdifellem1  19442  pmtrdifellem2  19443  pgpssslw  19580  lsmless1x  19610  lsmless2x  19611  lsmless12  19628  subglsm  19639  gsumval3lem2  19872  gsumzaddlem  19887  gsumzadd  19888  gsum2d  19938  dmdprdd  19967  dprdfeq0  19990  dprdspan  19995  dprdres  19996  dprdss  19997  dprdz  19998  subgdmdprd  20002  subgdprd  20003  dprdsn  20004  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  dprdsplit  20016  pgpfac1lem2  20043  pgpfac1lem3  20045  pgpfac1lem5  20047  subsubrng  20531  subsubrg  20566  subdrgint  20771  lspss  20970  lspun  20973  lsslsp  21001  lsslspOLD  21002  lmhmlsp  21036  lsmelval2  21072  lsmssspx  21075  lsppratlem2  21138  lsppratlem3  21139  lsppratlem4  21140  lbsextlem2  21149  lbsextlem3  21150  ocvlsp  21666  cssmre  21683  obselocv  21718  obslbs  21720  aspss  21866  mhpaddcl  22127  mhpinvcl  22128  mhpvscacl  22130  psdmullem  22141  toponmre  23068  neiint  23079  neiss  23084  lpss  23117  lpss3  23119  restopnb  23150  restfpw  23154  neitr  23155  restcls  23156  restntr  23157  restlp  23158  ordtbas  23167  pnfnei  23195  mnfnei  23196  iscnp4  23238  cnclsi  23247  isreg2  23352  discmp  23373  cmpcld  23377  uncmp  23378  sscmp  23380  hauscmplem  23381  cmpfi  23383  iunconnlem  23402  clsconn  23405  2ndcctbss  23430  restnlly  23457  llyrest  23460  nllyrest  23461  llyidm  23463  nllyidm  23464  cldllycmp  23470  dislly  23472  comppfsc  23507  llycmpkgen2  23525  ptbasfi  23556  txnlly  23612  txcmplem1  23616  tx1stc  23625  xkococnlem  23634  qtopval2  23671  basqtop  23686  tgqtop  23687  qtoprest  23692  kqreglem1  23716  kqreglem2  23717  kqnrmlem1  23718  kqnrmlem2  23719  fsubbas  23842  fgabs  23854  fbasrn  23859  trfil2  23862  trfg  23866  isufil2  23883  trufil  23885  ssufl  23893  ufileu  23894  filufint  23895  fmfnfmlem4  23932  fmfnfm  23933  flimss2  23947  flimss1  23948  fclsfnflim  24002  flimfnfcls  24003  fclscmp  24005  cnpfcfi  24015  alexsubALT  24026  clssubg  24084  clsnsg  24085  tsmsres  24119  ustexsym  24191  ustex2sym  24192  ustex3sym  24193  ustneism  24199  trust  24204  utoptop  24209  restutopopn  24213  utop2nei  24225  utopreg  24227  cfiluweak  24269  neipcfilu  24270  blssps  24399  blss  24400  blcld  24480  blsscls  24482  met1stc  24496  met2ndci  24497  metust  24533  cfilucfil  24534  restmetu  24545  tgqioo  24775  xrsblre  24787  reconnlem2  24803  xrge0gsumle  24809  xrge0tsms  24810  rescncf  24874  cnmpopc  24905  cnheibor  24932  cnllycmp  24933  lebnum  24941  phtpycn  24960  cfilfcls  25251  iscmet3lem2  25269  cmetss  25293  cncmet  25299  bcthlem4  25304  bcth3  25308  rrxcph  25369  rrxmetlem  25384  minveclem4a  25407  minveclem4  25409  ivthicc  25435  ovollb  25456  ovollb2lem  25465  ovollb2  25466  nulmbl2  25513  ioorcl2  25549  uniioombllem3  25562  uniioombllem4  25563  uniioombllem5  25564  opnmbllem  25578  volcn  25583  volivth  25584  mbfeqalem1  25618  itg10a  25687  mbfi1fseqlem4  25695  ditgcl  25835  ditgswap  25836  ditgsplitlem  25837  limcflf  25858  limcres  25863  dvbss  25878  dvbsss  25879  perfdvf  25880  dvreslem  25886  dvres2lem  25887  dvres3  25890  dvmptresicc  25893  dvcnp  25896  dvcnp2  25897  dvcn  25898  dvnff  25900  dvn2bss  25907  dvnres  25908  cpnord  25912  dvaddbr  25915  dvmulbr  25916  dvcobr  25923  dvnfre  25929  dvmptres2  25939  dvmptntr  25948  dvcnvlem  25953  dvcnv  25954  dvferm1lem  25961  dvferm2lem  25963  dvlip  25970  dvlipcn  25971  dvlip2  25972  c1liplem1  25973  dvgt0lem1  25979  lhop1lem  25990  lhop  25993  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcnvre  25996  dvfsumle  25998  dvfsumge  25999  dvfsumabs  26000  ftc1lem1  26012  ftc1lem2  26013  ftc1a  26014  ftc1lem4  26016  ftc2ditglem  26022  itgsubstlem  26025  ig1peu  26150  ig1pdvds  26155  taylfvallem1  26333  tayl0  26338  taylply2  26344  taylply2OLD  26345  taylply  26346  dvtaylp  26347  dvntaylp  26348  dvntaylp0  26349  taylthlem1  26350  ulmdvlem1  26378  ulmdvlem3  26380  psercn  26404  pserdvlem2  26406  abelth  26419  xrlimcnp  26945  lgamucov  27015  wilthlem2  27046  sqff1o  27159  chtublem  27188  pntlemq  27578  pntlemf  27582  ssslts1  27779  ssslts2  27780  cutbdaybnd  27801  cutbdaybnd2  27802  eqcuts3  27810  cofss  27936  coiniss  27937  bdaypw2bnd  28471  bdayfinbndlem1  28473  z12bdaylem2  28477  tglineintmo  28724  ttgcontlem1  28967  pthdlem1  29849  shintcli  31415  shub1  31468  mdslmd1lem1  32411  mdexchi  32421  chirredlem1  32476  mdsymlem5  32493  sumdmdii  32501  sumdmdlem2  32505  fnpreimac  32758  fsuppinisegfi  32775  xrge0infssd  32849  swrdrn3  33030  swrdf1  33031  swrdrndisj  33032  pwrssmgc  33075  xrge0tsmsd  33149  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  fldgenss  33392  fldgenssp  33394  linds2eq  33456  elrspunidl  33503  ssdifidllem  33531  ssdifidlprm  33533  mxidlprm  33545  ssmxidllem  33548  ssmxidl  33549  qsdrnglem2  33571  rprmdvdsprod  33609  ressply1evls1  33640  resssra  33746  lsssra  33747  exsslsb  33756  lbsdiflsp0  33786  dimkerim  33787  fedgmullem1  33789  fedgmullem2  33790  fedgmul  33791  dimlssid  33792  fldextrspunlsplem  33833  fldextrspunlsp  33834  fldextrspunlem1  33835  fldextrspundgdvdslem  33840  fldextrspundgdvds  33841  constr01  33902  constrmon  33904  constrextdg2lem  33908  constrfiss  33911  smatrcl  33956  locfinreflem  34000  cmpcref  34010  zarclsun  34030  zarclsiin  34031  zarclssn  34033  zarcmplem  34041  pnfneige0  34111  esum2d  34253  insiga  34297  sssigagen2  34306  dynkin  34327  dya2iocnei  34442  omsmon  34458  carsgclctunlem1  34477  carsggect  34478  omsmeas  34483  ftc2re  34758  fdvneggt  34760  fdvnegge  34762  reprsuc  34775  reprss  34777  reprlt  34779  reprinfz1  34782  logdivsqrle  34810  hgt750lemb  34816  bnj906  35088  bnj1020  35123  bnj1137  35153  bnj1408  35194  bnj1452  35210  rankval4b  35259  fineqvnttrclselem2  35282  erdszelem7  35395  erdszelem8  35396  erdsze2lem1  35401  connpconn  35433  cvmliftmolem1  35479  cvmlift2lem1  35500  cvmlift2lem9  35509  cvmlift2lem10  35510  cvmlift3lem6  35522  cvmlift3lem7  35523  satfsschain  35562  ss2mcls  35766  neibastop2lem  36558  fnemeet2  36565  fnejoin1  36566  ontgval  36629  ttcmin  36694  unbdqndv1  36784  opnmbllem0  37991  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  sstotbnd2  38109  heiborlem1  38146  heiborlem8  38153  intidl  38364  lsmsat  39468  lssats  39472  lpssat  39473  lssatle  39475  lssat  39476  lsatcvatlem  39509  paddss12  40279  paddasslem17  40296  pmodlem1  40306  pmod1i  40308  pmodl42N  40311  elpcliN  40353  pclfinN  40360  polcon3N  40377  polcon2N  40379  paddunN  40387  pclfinclN  40410  poml5N  40414  osumcllem1N  40416  osumcllem2N  40417  osumcllem3N  40418  pl42lem2N  40440  pl42lem4N  40442  cdlemn5pre  41660  dihord1  41678  dihord2a  41679  dihord2b  41680  dihord5b  41719  dochss  41825  dochdmj1  41850  djhsumss  41867  djhunssN  41869  dochexmidlem2  41921  lclkrslem1  41997  lclkrslem2  41998  lcfrlem2  42003  aks4d1p4  42532  aks4d1p5  42533  aks4d1p7  42536  aks4d1p8  42540  aks6d1c2  42583  sticksstones1  42599  unitscyglem5  42652  prjcrv0  43080  elrfi  43140  ismrcd1  43144  istopclsd  43146  mrefg2  43153  aomclem2  43501  aomclem6  43505  hbtlem6  43575  hbt  43576  oege2  43753  cantnftermord  43766  omabs2  43778  tfsconcat0b  43792  naddgeoa  43840  naddwordnexlem0  43842  naddwordnexlem1  43843  dfno2  43873  mptrcllem  44058  dfrcl2  44119  relexp0a  44161  trclimalb2  44171  frege81d  44192  k0004ss2  44597  imo72b2lem2  44612  imo72b2  44617  uzwo4  45502  ssin0  45504  ixpssmapc  45522  ssinc  45535  ssdec  45536  supxrre3  45773  uzfissfz  45774  ssuzfz  45797  supminfxr  45910  inficc  45982  ressiocsup  46002  ressioosup  46003  ressiooinf  46005  limccog  46068  limclner  46097  limsupres  46151  limsupresuz2  46155  limsupequzlem  46168  supcnvlimsup  46186  limsupgtlem  46223  liminfresuz2  46233  cncfmptssg  46317  cncfuni  46332  icccncfext  46333  dvresntr  46364  dvbdfbdioolem1  46374  dvdmsscn  46382  dvnxpaek  46388  dvnprodlem2  46393  stoweidlem59  46505  fourierdlem20  46573  fourierdlem42  46595  fourierdlem48  46600  fourierdlem49  46601  fourierdlem52  46604  fourierdlem58  46610  fourierdlem64  46616  fourierdlem73  46625  fourierdlem76  46628  fourierdlem80  46632  fourierdlem84  46636  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  fourierdlem113  46665  etransclem18  46698  ioorrnopnlem  46750  salincl  46770  intsal  46776  fsumlesge0  46823  sge0cl  46827  sge0supre  46835  sge0less  46838  sge0split  46855  sge0seq  46892  caragensspw  46955  omessre  46956  caragendifcl  46960  caratheodorylem1  46972  0ome  46975  omess0  46980  caragencmpl  46981  hoissrrn  46995  hoicvrrex  47002  ovnlecvr  47004  ovnsslelem  47006  ovnssle  47007  ovnsubaddlem1  47016  hoissrrn2  47024  hoidmv1lelem1  47037  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem4  47044  ovnlecvr2  47056  voncmpl  47067  hspmbl  47075  opnvonmbllem1  47078  ovolval5lem2  47099  ovolval5lem3  47100  vonioolem1  47126  pimdecfgtioc  47161  pimincfltioc  47162  pimdecfgtioo  47163  pimincfltioo  47164  issmflem  47173  cnfsmf  47186  incsmflem  47187  smfsssmf  47189  smfadd  47211  decsmflem  47212  smflim  47223  smfres  47236  smfmul  47241  smfpimbor1lem1  47244  smfco  47248  smfsuplem1  47257  smfsuplem3  47259  smflimsuplem1  47266  smflimsuplem4  47269  smflimsuplem7  47272  nndivides2  47844  cnneiima  49404  seposep  49413  iscnrm3rlem4  49430  iscnrm3llem1  49436  lubsscl  49447  glbsscl  49448  toplatglb  49488  setrecsss  50188  elpglem1  50198