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 585	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ⊆ wss 3903

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 3920

This theorem is referenced by:  sstrid  3947  sstrdi  3948  rabssrabd  4037  ssdif2d  4102  uniintsn  4942  funss  6519  fssxp  6697  knatar  7313  tfisi  7811  suppssov1  8149  suppssov2  8150  suppssfv  8154  tposss  8179  frrlem8  8245  tfrlem1  8317  omwordri  8509  oewordri  8530  oeeui  8540  oaabs2  8587  omopthlem1  8597  ecinxp  8741  sbthlem1  9027  dffi2  9338  hartogslem1  9459  cantnfcl  9588  cantnflt  9593  cantnfp1lem3  9601  cantnflem3  9612  cnfcom  9621  cnfcom3lem  9624  ttrcltr  9637  rankssb  9772  tskwe  9874  dfac12lem2  10067  dfac12lem3  10068  cfflb  10181  cfcof  10196  ssfin2  10242  hsmexlem4  10351  ttukeylem6  10436  ttukeylem7  10437  fpwwe2lem1  10554  fpwwe2lem7  10560  fpwwe2lem10  10563  fpwwe2lem11  10564  canthnumlem  10571  canthwelem  10573  canthwe  10574  canthp1lem2  10576  pwfseqlem5  10586  wunex2  10661  tsktrss  10684  inttsk  10697  uzwo3  12868  xrsupssd  13260  supicc  13429  supiccub  13430  supicclub  13431  ssfzunsnext  13497  seqsplit  13970  seqf1olem2a  13975  seqz  13985  swrdval2  14582  trrelssd  14908  rtrclreclem4  14996  sumss  15659  qshash  15762  incexc  15772  incexc2  15773  prodss  15882  rpnnen2lem11  16161  vdwlem1  16921  ramub1lem1  16966  imasaddvallem  17462  imasvscaf  17472  mrerintcl  17528  ismred2  17534  mremre  17535  mrcuni  17556  mressmrcd  17562  submrc  17563  mrissmrid  17576  mreexexlem2d  17580  isacs2  17588  isacs1i  17592  invss  17697  ssctr  17761  funcres2b  17833  isacs3lem  18477  acsfiindd  18488  acsmapd  18489  acsmap2d  18490  tsrdir  18539  subsubmgm  18647  subsubm  18753  gsumwspan  18783  subsubg  19091  subgint  19092  cntzidss  19281  symggen  19411  pmtrdifellem1  19417  pmtrdifellem2  19418  pgpssslw  19555  lsmless1x  19585  lsmless2x  19586  lsmless12  19603  subglsm  19614  gsumval3lem2  19847  gsumzaddlem  19862  gsumzadd  19863  gsum2d  19913  dmdprdd  19942  dprdfeq0  19965  dprdspan  19970  dprdres  19971  dprdss  19972  dprdz  19973  subgdmdprd  19977  subgdprd  19978  dprdsn  19979  dprd2dlem1  19984  dprd2da  19985  dmdprdsplit2lem  19988  dprdsplit  19991  pgpfac1lem2  20018  pgpfac1lem3  20020  pgpfac1lem5  20022  subsubrng  20508  subsubrg  20543  subdrgint  20748  lspss  20947  lspun  20950  lsslsp  20978  lsslspOLD  20979  lmhmlsp  21013  lsmelval2  21049  lsmssspx  21052  lsppratlem2  21115  lsppratlem3  21116  lsppratlem4  21117  lbsextlem2  21126  lbsextlem3  21127  ocvlsp  21643  cssmre  21660  obselocv  21695  obslbs  21697  aspss  21844  mhpaddcl  22106  mhpinvcl  22107  mhpvscacl  22109  psdmullem  22120  toponmre  23049  neiint  23060  neiss  23065  lpss  23098  lpss3  23100  restopnb  23131  restfpw  23135  neitr  23136  restcls  23137  restntr  23138  restlp  23139  ordtbas  23148  pnfnei  23176  mnfnei  23177  iscnp4  23219  cnclsi  23228  isreg2  23333  discmp  23354  cmpcld  23358  uncmp  23359  sscmp  23361  hauscmplem  23362  cmpfi  23364  iunconnlem  23383  clsconn  23386  2ndcctbss  23411  restnlly  23438  llyrest  23441  nllyrest  23442  llyidm  23444  nllyidm  23445  cldllycmp  23451  dislly  23453  comppfsc  23488  llycmpkgen2  23506  ptbasfi  23537  txnlly  23593  txcmplem1  23597  tx1stc  23606  xkococnlem  23615  qtopval2  23652  basqtop  23667  tgqtop  23668  qtoprest  23673  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  fsubbas  23823  fgabs  23835  fbasrn  23840  trfil2  23843  trfg  23847  isufil2  23864  trufil  23866  ssufl  23874  ufileu  23875  filufint  23876  fmfnfmlem4  23913  fmfnfm  23914  flimss2  23928  flimss1  23929  fclsfnflim  23983  flimfnfcls  23984  fclscmp  23986  cnpfcfi  23996  alexsubALT  24007  clssubg  24065  clsnsg  24066  tsmsres  24100  ustexsym  24172  ustex2sym  24173  ustex3sym  24174  ustneism  24180  trust  24185  utoptop  24190  restutopopn  24194  utop2nei  24206  utopreg  24208  cfiluweak  24250  neipcfilu  24251  blssps  24380  blss  24381  blcld  24461  blsscls  24463  met1stc  24477  met2ndci  24478  metust  24514  cfilucfil  24515  restmetu  24526  tgqioo  24756  xrsblre  24768  reconnlem2  24784  xrge0gsumle  24790  xrge0tsms  24791  rescncf  24858  cnmpopc  24890  cnheibor  24922  cnllycmp  24923  lebnum  24931  phtpycn  24950  cfilfcls  25242  iscmet3lem2  25260  cmetss  25284  cncmet  25290  bcthlem4  25295  bcth3  25299  rrxcph  25360  rrxmetlem  25375  minveclem4a  25398  minveclem4  25400  ivthicc  25427  ovollb  25448  ovollb2lem  25457  ovollb2  25458  nulmbl2  25505  ioorcl2  25541  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  opnmbllem  25570  volcn  25575  volivth  25576  mbfeqalem1  25610  itg10a  25679  mbfi1fseqlem4  25687  ditgcl  25827  ditgswap  25828  ditgsplitlem  25829  limcflf  25850  limcres  25855  dvbss  25870  dvbsss  25871  perfdvf  25872  dvreslem  25878  dvres2lem  25879  dvres3  25882  dvmptresicc  25885  dvcnp  25888  dvcnp2  25889  dvcnp2OLD  25890  dvcn  25891  dvnff  25893  dvn2bss  25900  dvnres  25901  cpnord  25905  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcobr  25917  dvcobrOLD  25918  dvnfre  25924  dvmptres2  25934  dvmptntr  25943  dvcnvlem  25948  dvcnv  25949  dvferm1lem  25956  dvferm2lem  25958  dvlip  25966  dvlipcn  25967  dvlip2  25968  c1liplem1  25969  dvgt0lem1  25975  lhop1lem  25986  lhop  25989  dvcnvrelem1  25990  dvcnvrelem2  25991  dvcnvre  25992  dvfsumle  25994  dvfsumleOLD  25995  dvfsumge  25996  dvfsumabs  25997  ftc1lem1  26010  ftc1lem2  26011  ftc1a  26012  ftc1lem4  26014  ftc2ditglem  26020  itgsubstlem  26023  ig1peu  26148  ig1pdvds  26153  taylfvallem1  26332  tayl0  26337  taylply2  26343  taylply2OLD  26344  taylply  26345  dvtaylp  26346  dvntaylp  26347  dvntaylp0  26348  taylthlem1  26349  ulmdvlem1  26377  ulmdvlem3  26379  psercn  26404  pserdvlem2  26406  abelth  26419  xrlimcnp  26946  lgamucov  27016  wilthlem2  27047  sqff1o  27160  chtublem  27190  pntlemq  27580  pntlemf  27584  ssslts1  27781  ssslts2  27782  cutbdaybnd  27803  cutbdaybnd2  27804  eqcuts3  27812  cofss  27938  coiniss  27939  bdaypw2bnd  28473  bdayfinbndlem1  28475  z12bdaylem2  28479  tglineintmo  28726  ttgcontlem1  28969  pthdlem1  29851  shintcli  31416  shub1  31469  mdslmd1lem1  32412  mdexchi  32422  chirredlem1  32477  mdsymlem5  32494  sumdmdii  32502  sumdmdlem2  32506  fnpreimac  32759  fsuppinisegfi  32776  xrge0infssd  32851  swrdrn3  33047  swrdf1  33048  swrdrndisj  33049  pwrssmgc  33092  xrge0tsmsd  33166  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  fldgenss  33409  fldgenssp  33411  linds2eq  33473  elrspunidl  33520  ssdifidllem  33548  ssdifidlprm  33550  mxidlprm  33562  ssmxidllem  33565  ssmxidl  33566  qsdrnglem2  33588  rprmdvdsprod  33626  ressply1evls1  33657  resssra  33763  lsssra  33764  exsslsb  33773  lbsdiflsp0  33803  dimkerim  33804  fedgmullem1  33806  fedgmullem2  33807  fedgmul  33808  dimlssid  33809  fldextrspunlsplem  33850  fldextrspunlsp  33851  fldextrspunlem1  33852  fldextrspundgdvdslem  33857  fldextrspundgdvds  33858  constr01  33919  constrmon  33921  constrextdg2lem  33925  constrfiss  33928  smatrcl  33973  locfinreflem  34017  cmpcref  34027  zarclsun  34047  zarclsiin  34048  zarclssn  34050  zarcmplem  34058  pnfneige0  34128  esum2d  34270  insiga  34314  sssigagen2  34323  dynkin  34344  dya2iocnei  34459  omsmon  34475  carsgclctunlem1  34494  carsggect  34495  omsmeas  34500  ftc2re  34775  fdvneggt  34777  fdvnegge  34779  reprsuc  34792  reprss  34794  reprlt  34796  reprinfz1  34799  logdivsqrle  34827  hgt750lemb  34833  bnj906  35105  bnj1020  35140  bnj1137  35170  bnj1408  35211  bnj1452  35227  rankval4b  35275  fineqvnttrclselem2  35297  erdszelem7  35410  erdszelem8  35411  erdsze2lem1  35416  connpconn  35448  cvmliftmolem1  35494  cvmlift2lem1  35515  cvmlift2lem9  35524  cvmlift2lem10  35525  cvmlift3lem6  35537  cvmlift3lem7  35538  satfsschain  35577  ss2mcls  35781  neibastop2lem  36573  fnemeet2  36580  fnejoin1  36581  ontgval  36644  unbdqndv1  36727  opnmbllem0  37901  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  sstotbnd2  38019  heiborlem1  38056  heiborlem8  38063  intidl  38274  lsmsat  39378  lssats  39382  lpssat  39383  lssatle  39385  lssat  39386  lsatcvatlem  39419  paddss12  40189  paddasslem17  40206  pmodlem1  40216  pmod1i  40218  pmodl42N  40221  elpcliN  40263  pclfinN  40270  polcon3N  40287  polcon2N  40289  paddunN  40297  pclfinclN  40320  poml5N  40324  osumcllem1N  40326  osumcllem2N  40327  osumcllem3N  40328  pl42lem2N  40350  pl42lem4N  40352  cdlemn5pre  41570  dihord1  41588  dihord2a  41589  dihord2b  41590  dihord5b  41629  dochss  41735  dochdmj1  41760  djhsumss  41777  djhunssN  41779  dochexmidlem2  41831  lclkrslem1  41907  lclkrslem2  41908  lcfrlem2  41913  aks4d1p4  42443  aks4d1p5  42444  aks4d1p7  42447  aks4d1p8  42451  aks6d1c2  42494  sticksstones1  42510  unitscyglem5  42563  prjcrv0  42985  elrfi  43045  ismrcd1  43049  istopclsd  43051  mrefg2  43058  aomclem2  43406  aomclem6  43410  hbtlem6  43480  hbt  43481  oege2  43658  cantnftermord  43671  omabs2  43683  tfsconcat0b  43697  naddgeoa  43745  naddwordnexlem0  43747  naddwordnexlem1  43748  dfno2  43778  mptrcllem  43963  dfrcl2  44024  relexp0a  44066  trclimalb2  44076  frege81d  44097  k0004ss2  44502  imo72b2lem2  44517  imo72b2  44522  uzwo4  45407  ssin0  45409  ixpssmapc  45427  ssinc  45440  ssdec  45441  supxrre3  45678  uzfissfz  45679  ssuzfz  45702  supminfxr  45816  inficc  45888  ressiocsup  45908  ressioosup  45909  ressiooinf  45911  limccog  45974  limclner  46003  limsupres  46057  limsupresuz2  46061  limsupequzlem  46074  supcnvlimsup  46092  limsupgtlem  46129  liminfresuz2  46139  cncfmptssg  46223  cncfuni  46238  icccncfext  46239  dvresntr  46270  dvbdfbdioolem1  46280  dvdmsscn  46288  dvnxpaek  46294  dvnprodlem2  46299  stoweidlem59  46411  fourierdlem20  46479  fourierdlem42  46501  fourierdlem48  46506  fourierdlem49  46507  fourierdlem52  46510  fourierdlem58  46516  fourierdlem64  46522  fourierdlem73  46531  fourierdlem76  46534  fourierdlem80  46538  fourierdlem84  46542  fourierdlem93  46551  fourierdlem103  46561  fourierdlem104  46562  fourierdlem113  46571  etransclem18  46604  ioorrnopnlem  46656  salincl  46676  intsal  46682  fsumlesge0  46729  sge0cl  46733  sge0supre  46741  sge0less  46744  sge0split  46761  sge0seq  46798  caragensspw  46861  omessre  46862  caragendifcl  46866  caratheodorylem1  46878  0ome  46881  omess0  46886  caragencmpl  46887  hoicvr  46900  hoissrrn  46901  hoicvrrex  46908  ovnlecvr  46910  ovnsslelem  46912  ovnssle  46913  ovnsubaddlem1  46922  hoissrrn2  46930  hoidmv1lelem1  46943  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem4  46950  ovnlecvr2  46962  voncmpl  46973  hspmbl  46981  opnvonmbllem1  46984  ovolval5lem2  47005  ovolval5lem3  47006  vonioolem1  47032  pimdecfgtioc  47067  pimincfltioc  47068  pimdecfgtioo  47069  pimincfltioo  47070  issmflem  47079  cnfsmf  47092  incsmflem  47093  smfsssmf  47095  smfadd  47117  decsmflem  47118  smflim  47129  smfres  47142  smfmul  47147  smfpimbor1lem1  47150  smfco  47154  smfsuplem1  47163  smfsuplem3  47165  smflimsuplem1  47172  smflimsuplem4  47175  smflimsuplem7  47178  cnneiima  49270  seposep  49279  iscnrm3rlem4  49296  iscnrm3llem1  49302  lubsscl  49313  glbsscl  49314  toplatglb  49354  setrecsss  50054  elpglem1  50064