Theorem sstrd 3944

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

Syntax hints:   → wi 4   ⊆ wss 3901

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

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

This theorem is referenced by:  sstrid  3945  sstrdi  3946  rabssrabd  4035  ssdif2d  4100  uniintsn  4940  funss  6511  fssxp  6689  knatar  7303  tfisi  7801  suppssov1  8139  suppssov2  8140  suppssfv  8144  tposss  8169  frrlem8  8235  tfrlem1  8307  omwordri  8499  oewordri  8520  oeeui  8530  oaabs2  8577  omopthlem1  8587  ecinxp  8729  sbthlem1  9015  dffi2  9326  hartogslem1  9447  cantnfcl  9576  cantnflt  9581  cantnfp1lem3  9589  cantnflem3  9600  cnfcom  9609  cnfcom3lem  9612  ttrcltr  9625  rankssb  9760  tskwe  9862  dfac12lem2  10055  dfac12lem3  10056  cfflb  10169  cfcof  10184  ssfin2  10230  hsmexlem4  10339  ttukeylem6  10424  ttukeylem7  10425  fpwwe2lem1  10542  fpwwe2lem7  10548  fpwwe2lem10  10551  fpwwe2lem11  10552  canthnumlem  10559  canthwelem  10561  canthwe  10562  canthp1lem2  10564  pwfseqlem5  10574  wunex2  10649  tsktrss  10672  inttsk  10685  uzwo3  12856  xrsupssd  13248  supicc  13417  supiccub  13418  supicclub  13419  ssfzunsnext  13485  seqsplit  13958  seqf1olem2a  13963  seqz  13973  swrdval2  14570  trrelssd  14896  rtrclreclem4  14984  sumss  15647  qshash  15750  incexc  15760  incexc2  15761  prodss  15870  rpnnen2lem11  16149  vdwlem1  16909  ramub1lem1  16954  imasaddvallem  17450  imasvscaf  17460  mrerintcl  17516  ismred2  17522  mremre  17523  mrcuni  17544  mressmrcd  17550  submrc  17551  mrissmrid  17564  mreexexlem2d  17568  isacs2  17576  isacs1i  17580  invss  17685  ssctr  17749  funcres2b  17821  isacs3lem  18465  acsfiindd  18476  acsmapd  18477  acsmap2d  18478  tsrdir  18527  subsubmgm  18635  subsubm  18741  gsumwspan  18771  subsubg  19079  subgint  19080  cntzidss  19269  symggen  19399  pmtrdifellem1  19405  pmtrdifellem2  19406  pgpssslw  19543  lsmless1x  19573  lsmless2x  19574  lsmless12  19591  subglsm  19602  gsumval3lem2  19835  gsumzaddlem  19850  gsumzadd  19851  gsum2d  19901  dmdprdd  19930  dprdfeq0  19953  dprdspan  19958  dprdres  19959  dprdss  19960  dprdz  19961  subgdmdprd  19965  subgdprd  19966  dprdsn  19967  dprd2dlem1  19972  dprd2da  19973  dmdprdsplit2lem  19976  dprdsplit  19979  pgpfac1lem2  20006  pgpfac1lem3  20008  pgpfac1lem5  20010  subsubrng  20496  subsubrg  20531  subdrgint  20736  lspss  20935  lspun  20938  lsslsp  20966  lsslspOLD  20967  lmhmlsp  21001  lsmelval2  21037  lsmssspx  21040  lsppratlem2  21103  lsppratlem3  21104  lsppratlem4  21105  lbsextlem2  21114  lbsextlem3  21115  ocvlsp  21631  cssmre  21648  obselocv  21683  obslbs  21685  aspss  21832  mhpaddcl  22094  mhpinvcl  22095  mhpvscacl  22097  psdmullem  22108  toponmre  23037  neiint  23048  neiss  23053  lpss  23086  lpss3  23088  restopnb  23119  restfpw  23123  neitr  23124  restcls  23125  restntr  23126  restlp  23127  ordtbas  23136  pnfnei  23164  mnfnei  23165  iscnp4  23207  cnclsi  23216  isreg2  23321  discmp  23342  cmpcld  23346  uncmp  23347  sscmp  23349  hauscmplem  23350  cmpfi  23352  iunconnlem  23371  clsconn  23374  2ndcctbss  23399  restnlly  23426  llyrest  23429  nllyrest  23430  llyidm  23432  nllyidm  23433  cldllycmp  23439  dislly  23441  comppfsc  23476  llycmpkgen2  23494  ptbasfi  23525  txnlly  23581  txcmplem1  23585  tx1stc  23594  xkococnlem  23603  qtopval2  23640  basqtop  23655  tgqtop  23656  qtoprest  23661  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  fsubbas  23811  fgabs  23823  fbasrn  23828  trfil2  23831  trfg  23835  isufil2  23852  trufil  23854  ssufl  23862  ufileu  23863  filufint  23864  fmfnfmlem4  23901  fmfnfm  23902  flimss2  23916  flimss1  23917  fclsfnflim  23971  flimfnfcls  23972  fclscmp  23974  cnpfcfi  23984  alexsubALT  23995  clssubg  24053  clsnsg  24054  tsmsres  24088  ustexsym  24160  ustex2sym  24161  ustex3sym  24162  ustneism  24168  trust  24173  utoptop  24178  restutopopn  24182  utop2nei  24194  utopreg  24196  cfiluweak  24238  neipcfilu  24239  blssps  24368  blss  24369  blcld  24449  blsscls  24451  met1stc  24465  met2ndci  24466  metust  24502  cfilucfil  24503  restmetu  24514  tgqioo  24744  xrsblre  24756  reconnlem2  24772  xrge0gsumle  24778  xrge0tsms  24779  rescncf  24846  cnmpopc  24878  cnheibor  24910  cnllycmp  24911  lebnum  24919  phtpycn  24938  cfilfcls  25230  iscmet3lem2  25248  cmetss  25272  cncmet  25278  bcthlem4  25283  bcth3  25287  rrxcph  25348  rrxmetlem  25363  minveclem4a  25386  minveclem4  25388  ivthicc  25415  ovollb  25436  ovollb2lem  25445  ovollb2  25446  nulmbl2  25493  ioorcl2  25529  uniioombllem3  25542  uniioombllem4  25543  uniioombllem5  25544  opnmbllem  25558  volcn  25563  volivth  25564  mbfeqalem1  25598  itg10a  25667  mbfi1fseqlem4  25675  ditgcl  25815  ditgswap  25816  ditgsplitlem  25817  limcflf  25838  limcres  25843  dvbss  25858  dvbsss  25859  perfdvf  25860  dvreslem  25866  dvres2lem  25867  dvres3  25870  dvmptresicc  25873  dvcnp  25876  dvcnp2  25877  dvcnp2OLD  25878  dvcn  25879  dvnff  25881  dvn2bss  25888  dvnres  25889  cpnord  25893  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcobr  25905  dvcobrOLD  25906  dvnfre  25912  dvmptres2  25922  dvmptntr  25931  dvcnvlem  25936  dvcnv  25937  dvferm1lem  25944  dvferm2lem  25946  dvlip  25954  dvlipcn  25955  dvlip2  25956  c1liplem1  25957  dvgt0lem1  25963  lhop1lem  25974  lhop  25977  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcnvre  25980  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvfsumabs  25985  ftc1lem1  25998  ftc1lem2  25999  ftc1a  26000  ftc1lem4  26002  ftc2ditglem  26008  itgsubstlem  26011  ig1peu  26136  ig1pdvds  26141  taylfvallem1  26320  tayl0  26325  taylply2  26331  taylply2OLD  26332  taylply  26333  dvtaylp  26334  dvntaylp  26335  dvntaylp0  26336  taylthlem1  26337  ulmdvlem1  26365  ulmdvlem3  26367  psercn  26392  pserdvlem2  26394  abelth  26407  xrlimcnp  26934  lgamucov  27004  wilthlem2  27035  sqff1o  27148  chtublem  27178  pntlemq  27568  pntlemf  27572  ssslts1  27769  ssslts2  27770  cutbdaybnd  27791  cutbdaybnd2  27792  eqcuts3  27800  cofss  27926  coiniss  27927  bdaypw2bnd  28461  bdayfinbndlem1  28463  z12bdaylem2  28467  tglineintmo  28714  ttgcontlem1  28957  pthdlem1  29839  shintcli  31404  shub1  31457  mdslmd1lem1  32400  mdexchi  32410  chirredlem1  32465  mdsymlem5  32482  sumdmdii  32490  sumdmdlem2  32494  fnpreimac  32749  fsuppinisegfi  32766  xrge0infssd  32841  swrdrn3  33037  swrdf1  33038  swrdrndisj  33039  pwrssmgc  33082  xrge0tsmsd  33155  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  fldgenss  33398  fldgenssp  33400  linds2eq  33462  elrspunidl  33509  ssdifidllem  33537  ssdifidlprm  33539  mxidlprm  33551  ssmxidllem  33554  ssmxidl  33555  qsdrnglem2  33577  rprmdvdsprod  33615  ressply1evls1  33646  resssra  33743  lsssra  33744  exsslsb  33753  lbsdiflsp0  33783  dimkerim  33784  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  dimlssid  33789  fldextrspunlsplem  33830  fldextrspunlsp  33831  fldextrspunlem1  33832  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  constr01  33899  constrmon  33901  constrextdg2lem  33905  constrfiss  33908  smatrcl  33953  locfinreflem  33997  cmpcref  34007  zarclsun  34027  zarclsiin  34028  zarclssn  34030  zarcmplem  34038  pnfneige0  34108  esum2d  34250  insiga  34294  sssigagen2  34303  dynkin  34324  dya2iocnei  34439  omsmon  34455  carsgclctunlem1  34474  carsggect  34475  omsmeas  34480  ftc2re  34755  fdvneggt  34757  fdvnegge  34759  reprsuc  34772  reprss  34774  reprlt  34776  reprinfz1  34779  logdivsqrle  34807  hgt750lemb  34813  bnj906  35086  bnj1020  35121  bnj1137  35151  bnj1408  35192  bnj1452  35208  rankval4b  35256  fineqvnttrclselem2  35278  erdszelem7  35391  erdszelem8  35392  erdsze2lem1  35397  connpconn  35429  cvmliftmolem1  35475  cvmlift2lem1  35496  cvmlift2lem9  35505  cvmlift2lem10  35506  cvmlift3lem6  35518  cvmlift3lem7  35519  satfsschain  35558  ss2mcls  35762  neibastop2lem  36554  fnemeet2  36561  fnejoin1  36562  ontgval  36625  unbdqndv1  36708  opnmbllem0  37853  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  sstotbnd2  37971  heiborlem1  38008  heiborlem8  38015  intidl  38226  lsmsat  39264  lssats  39268  lpssat  39269  lssatle  39271  lssat  39272  lsatcvatlem  39305  paddss12  40075  paddasslem17  40092  pmodlem1  40102  pmod1i  40104  pmodl42N  40107  elpcliN  40149  pclfinN  40156  polcon3N  40173  polcon2N  40175  paddunN  40183  pclfinclN  40206  poml5N  40210  osumcllem1N  40212  osumcllem2N  40213  osumcllem3N  40214  pl42lem2N  40236  pl42lem4N  40238  cdlemn5pre  41456  dihord1  41474  dihord2a  41475  dihord2b  41476  dihord5b  41515  dochss  41621  dochdmj1  41646  djhsumss  41663  djhunssN  41665  dochexmidlem2  41717  lclkrslem1  41793  lclkrslem2  41794  lcfrlem2  41799  aks4d1p4  42329  aks4d1p5  42330  aks4d1p7  42333  aks4d1p8  42337  aks6d1c2  42380  sticksstones1  42396  unitscyglem5  42449  prjcrv0  42872  elrfi  42932  ismrcd1  42936  istopclsd  42938  mrefg2  42945  aomclem2  43293  aomclem6  43297  hbtlem6  43367  hbt  43368  oege2  43545  cantnftermord  43558  omabs2  43570  tfsconcat0b  43584  naddgeoa  43632  naddwordnexlem0  43634  naddwordnexlem1  43635  dfno2  43665  mptrcllem  43850  dfrcl2  43911  relexp0a  43953  trclimalb2  43963  frege81d  43984  k0004ss2  44389  imo72b2lem2  44404  imo72b2  44409  uzwo4  45294  ssin0  45296  ixpssmapc  45314  ssinc  45327  ssdec  45328  supxrre3  45566  uzfissfz  45567  ssuzfz  45590  supminfxr  45704  inficc  45776  ressiocsup  45796  ressioosup  45797  ressiooinf  45799  limccog  45862  limclner  45891  limsupres  45945  limsupresuz2  45949  limsupequzlem  45962  supcnvlimsup  45980  limsupgtlem  46017  liminfresuz2  46027  cncfmptssg  46111  cncfuni  46126  icccncfext  46127  dvresntr  46158  dvbdfbdioolem1  46168  dvdmsscn  46176  dvnxpaek  46182  dvnprodlem2  46187  stoweidlem59  46299  fourierdlem20  46367  fourierdlem42  46389  fourierdlem48  46394  fourierdlem49  46395  fourierdlem52  46398  fourierdlem58  46404  fourierdlem64  46410  fourierdlem73  46419  fourierdlem76  46422  fourierdlem80  46426  fourierdlem84  46430  fourierdlem93  46439  fourierdlem103  46449  fourierdlem104  46450  fourierdlem113  46459  etransclem18  46492  ioorrnopnlem  46544  salincl  46564  intsal  46570  fsumlesge0  46617  sge0cl  46621  sge0supre  46629  sge0less  46632  sge0split  46649  sge0seq  46686  caragensspw  46749  omessre  46750  caragendifcl  46754  caratheodorylem1  46766  0ome  46769  omess0  46774  caragencmpl  46775  hoicvr  46788  hoissrrn  46789  hoicvrrex  46796  ovnlecvr  46798  ovnsslelem  46800  ovnssle  46801  ovnsubaddlem1  46810  hoissrrn2  46818  hoidmv1lelem1  46831  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem4  46838  ovnlecvr2  46850  voncmpl  46861  hspmbl  46869  opnvonmbllem1  46872  ovolval5lem2  46893  ovolval5lem3  46894  vonioolem1  46920  pimdecfgtioc  46955  pimincfltioc  46956  pimdecfgtioo  46957  pimincfltioo  46958  issmflem  46967  cnfsmf  46980  incsmflem  46981  smfsssmf  46983  smfadd  47005  decsmflem  47006  smflim  47017  smfres  47030  smfmul  47035  smfpimbor1lem1  47038  smfco  47042  smfsuplem1  47051  smfsuplem3  47053  smflimsuplem1  47060  smflimsuplem4  47063  smflimsuplem7  47066  cnneiima  49158  seposep  49167  iscnrm3rlem4  49184  iscnrm3llem1  49190  lubsscl  49201  glbsscl  49202  toplatglb  49242  setrecsss  49942  elpglem1  49952