Theorem sstrd 3932

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

Syntax hints:   → wi 4   ⊆ wss 3889

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 3906

This theorem is referenced by:  sstrid  3933  sstrdi  3934  rabssrabd  4023  ssdif2d  4088  uniintsn  4927  funss  6517  fssxp  6695  knatar  7312  tfisi  7810  suppssov1  8147  suppssov2  8148  suppssfv  8152  tposss  8177  frrlem8  8243  tfrlem1  8315  omwordri  8507  oewordri  8528  oeeui  8538  oaabs2  8585  omopthlem1  8595  ecinxp  8739  sbthlem1  9025  dffi2  9336  hartogslem1  9457  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  12893  xrsupssd  13285  supicc  13454  supiccub  13455  supicclub  13456  ssfzunsnext  13523  seqsplit  13997  seqf1olem2a  14002  seqz  14012  swrdval2  14609  trrelssd  14935  rtrclreclem4  15023  sumss  15686  qshash  15790  incexc  15802  incexc2  15803  prodss  15912  rpnnen2lem11  16191  vdwlem1  16952  ramub1lem1  16997  imasaddvallem  17493  imasvscaf  17503  mrerintcl  17559  ismred2  17565  mremre  17566  mrcuni  17587  mressmrcd  17593  submrc  17594  mrissmrid  17607  mreexexlem2d  17611  isacs2  17619  isacs1i  17623  invss  17728  ssctr  17792  funcres2b  17864  isacs3lem  18508  acsfiindd  18519  acsmapd  18520  acsmap2d  18521  tsrdir  18570  subsubmgm  18678  subsubm  18784  gsumwspan  18814  subsubg  19125  subgint  19126  cntzidss  19315  symggen  19445  pmtrdifellem1  19451  pmtrdifellem2  19452  pgpssslw  19589  lsmless1x  19619  lsmless2x  19620  lsmless12  19637  subglsm  19648  gsumval3lem2  19881  gsumzaddlem  19896  gsumzadd  19897  gsum2d  19947  dmdprdd  19976  dprdfeq0  19999  dprdspan  20004  dprdres  20005  dprdss  20006  dprdz  20007  subgdmdprd  20011  subgdprd  20012  dprdsn  20013  dprd2dlem1  20018  dprd2da  20019  dmdprdsplit2lem  20022  dprdsplit  20025  pgpfac1lem2  20052  pgpfac1lem3  20054  pgpfac1lem5  20056  subsubrng  20540  subsubrg  20575  subdrgint  20780  lspss  20979  lspun  20982  lsslsp  21010  lmhmlsp  21044  lsmelval2  21080  lsmssspx  21083  lsppratlem2  21146  lsppratlem3  21147  lsppratlem4  21148  lbsextlem2  21157  lbsextlem3  21158  ocvlsp  21656  cssmre  21673  obselocv  21708  obslbs  21710  aspss  21856  mhpaddcl  22117  mhpinvcl  22118  mhpvscacl  22120  psdmullem  22131  toponmre  23058  neiint  23069  neiss  23074  lpss  23107  lpss3  23109  restopnb  23140  restfpw  23144  neitr  23145  restcls  23146  restntr  23147  restlp  23148  ordtbas  23157  pnfnei  23185  mnfnei  23186  iscnp4  23228  cnclsi  23237  isreg2  23342  discmp  23363  cmpcld  23367  uncmp  23368  sscmp  23370  hauscmplem  23371  cmpfi  23373  iunconnlem  23392  clsconn  23395  2ndcctbss  23420  restnlly  23447  llyrest  23450  nllyrest  23451  llyidm  23453  nllyidm  23454  cldllycmp  23460  dislly  23462  comppfsc  23497  llycmpkgen2  23515  ptbasfi  23546  txnlly  23602  txcmplem1  23606  tx1stc  23615  xkococnlem  23624  qtopval2  23661  basqtop  23676  tgqtop  23677  qtoprest  23682  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  fsubbas  23832  fgabs  23844  fbasrn  23849  trfil2  23852  trfg  23856  isufil2  23873  trufil  23875  ssufl  23883  ufileu  23884  filufint  23885  fmfnfmlem4  23922  fmfnfm  23923  flimss2  23937  flimss1  23938  fclsfnflim  23992  flimfnfcls  23993  fclscmp  23995  cnpfcfi  24005  alexsubALT  24016  clssubg  24074  clsnsg  24075  tsmsres  24109  ustexsym  24181  ustex2sym  24182  ustex3sym  24183  ustneism  24189  trust  24194  utoptop  24199  restutopopn  24203  utop2nei  24215  utopreg  24217  cfiluweak  24259  neipcfilu  24260  blssps  24389  blss  24390  blcld  24470  blsscls  24472  met1stc  24486  met2ndci  24487  metust  24523  cfilucfil  24524  restmetu  24535  tgqioo  24765  xrsblre  24777  reconnlem2  24793  xrge0gsumle  24799  xrge0tsms  24800  rescncf  24864  cnmpopc  24895  cnheibor  24922  cnllycmp  24923  lebnum  24931  phtpycn  24950  cfilfcls  25241  iscmet3lem2  25259  cmetss  25283  cncmet  25289  bcthlem4  25294  bcth3  25298  rrxcph  25359  rrxmetlem  25374  minveclem4a  25397  minveclem4  25399  ivthicc  25425  ovollb  25446  ovollb2lem  25455  ovollb2  25456  nulmbl2  25503  ioorcl2  25539  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  opnmbllem  25568  volcn  25573  volivth  25574  mbfeqalem1  25608  itg10a  25677  mbfi1fseqlem4  25685  ditgcl  25825  ditgswap  25826  ditgsplitlem  25827  limcflf  25848  limcres  25853  dvbss  25868  dvbsss  25869  perfdvf  25870  dvreslem  25876  dvres2lem  25877  dvres3  25880  dvmptresicc  25883  dvcnp  25886  dvcnp2  25887  dvcn  25888  dvnff  25890  dvn2bss  25897  dvnres  25898  cpnord  25902  dvaddbr  25905  dvmulbr  25906  dvcobr  25913  dvnfre  25919  dvmptres2  25929  dvmptntr  25938  dvcnvlem  25943  dvcnv  25944  dvferm1lem  25951  dvferm2lem  25953  dvlip  25960  dvlipcn  25961  dvlip2  25962  c1liplem1  25963  dvgt0lem1  25969  lhop1lem  25980  lhop  25983  dvcnvrelem1  25984  dvcnvrelem2  25985  dvcnvre  25986  dvfsumle  25988  dvfsumge  25989  dvfsumabs  25990  ftc1lem1  26002  ftc1lem2  26003  ftc1a  26004  ftc1lem4  26006  ftc2ditglem  26012  itgsubstlem  26015  ig1peu  26140  ig1pdvds  26145  taylfvallem1  26322  tayl0  26327  taylply2  26333  taylply  26334  dvtaylp  26335  dvntaylp  26336  dvntaylp0  26337  taylthlem1  26338  ulmdvlem1  26365  ulmdvlem3  26367  psercn  26391  pserdvlem2  26393  abelth  26406  xrlimcnp  26932  lgamucov  27001  wilthlem2  27032  sqff1o  27145  chtublem  27174  pntlemq  27564  pntlemf  27568  ssslts1  27765  ssslts2  27766  cutbdaybnd  27787  cutbdaybnd2  27788  eqcuts3  27796  cofss  27922  coiniss  27923  bdaypw2bnd  28457  bdayfinbndlem1  28459  z12bdaylem2  28463  tglineintmo  28710  ttgcontlem1  28953  pthdlem1  29834  shintcli  31400  shub1  31453  mdslmd1lem1  32396  mdexchi  32406  chirredlem1  32461  mdsymlem5  32478  sumdmdii  32486  sumdmdlem2  32490  fnpreimac  32743  fsuppinisegfi  32760  xrge0infssd  32834  swrdrn3  33015  swrdf1  33016  swrdrndisj  33017  pwrssmgc  33060  xrge0tsmsd  33134  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  fldgenss  33377  fldgenssp  33379  linds2eq  33441  elrspunidl  33488  ssdifidllem  33516  ssdifidlprm  33518  mxidlprm  33530  ssmxidllem  33533  ssmxidl  33534  qsdrnglem2  33556  rprmdvdsprod  33594  ressply1evls1  33625  resssra  33731  lsssra  33732  exsslsb  33741  lbsdiflsp0  33770  dimkerim  33771  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  dimlssid  33776  fldextrspunlsplem  33817  fldextrspunlsp  33818  fldextrspunlem1  33819  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  constr01  33886  constrmon  33888  constrextdg2lem  33892  constrfiss  33895  smatrcl  33940  locfinreflem  33984  cmpcref  33994  zarclsun  34014  zarclsiin  34015  zarclssn  34017  zarcmplem  34025  pnfneige0  34095  esum2d  34237  insiga  34281  sssigagen2  34290  dynkin  34311  dya2iocnei  34426  omsmon  34442  carsgclctunlem1  34461  carsggect  34462  omsmeas  34467  ftc2re  34742  fdvneggt  34744  fdvnegge  34746  reprsuc  34759  reprss  34761  reprlt  34763  reprinfz1  34766  logdivsqrle  34794  hgt750lemb  34800  bnj906  35072  bnj1020  35107  bnj1137  35137  bnj1408  35178  bnj1452  35194  rankval4b  35243  fineqvnttrclselem2  35266  erdszelem7  35379  erdszelem8  35380  erdsze2lem1  35385  connpconn  35417  cvmliftmolem1  35463  cvmlift2lem1  35484  cvmlift2lem9  35493  cvmlift2lem10  35494  cvmlift3lem6  35506  cvmlift3lem7  35507  satfsschain  35546  ss2mcls  35750  neibastop2lem  36542  fnemeet2  36549  fnejoin1  36550  ontgval  36613  ttcmin  36678  unbdqndv1  36768  opnmbllem0  37977  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  sstotbnd2  38095  heiborlem1  38132  heiborlem8  38139  intidl  38350  lsmsat  39454  lssats  39458  lpssat  39459  lssatle  39461  lssat  39462  lsatcvatlem  39495  paddss12  40265  paddasslem17  40282  pmodlem1  40292  pmod1i  40294  pmodl42N  40297  elpcliN  40339  pclfinN  40346  polcon3N  40363  polcon2N  40365  paddunN  40373  pclfinclN  40396  poml5N  40400  osumcllem1N  40402  osumcllem2N  40403  osumcllem3N  40404  pl42lem2N  40426  pl42lem4N  40428  cdlemn5pre  41646  dihord1  41664  dihord2a  41665  dihord2b  41666  dihord5b  41705  dochss  41811  dochdmj1  41836  djhsumss  41853  djhunssN  41855  dochexmidlem2  41907  lclkrslem1  41983  lclkrslem2  41984  lcfrlem2  41989  aks4d1p4  42518  aks4d1p5  42519  aks4d1p7  42522  aks4d1p8  42526  aks6d1c2  42569  sticksstones1  42585  unitscyglem5  42638  prjcrv0  43066  elrfi  43126  ismrcd1  43130  istopclsd  43132  mrefg2  43139  aomclem2  43483  aomclem6  43487  hbtlem6  43557  hbt  43558  oege2  43735  cantnftermord  43748  omabs2  43760  tfsconcat0b  43774  naddgeoa  43822  naddwordnexlem0  43824  naddwordnexlem1  43825  dfno2  43855  mptrcllem  44040  dfrcl2  44101  relexp0a  44143  trclimalb2  44153  frege81d  44174  k0004ss2  44579  imo72b2lem2  44594  imo72b2  44599  uzwo4  45484  ssin0  45486  ixpssmapc  45504  ssinc  45517  ssdec  45518  supxrre3  45755  uzfissfz  45756  ssuzfz  45779  supminfxr  45892  inficc  45964  ressiocsup  45984  ressioosup  45985  ressiooinf  45987  limccog  46050  limclner  46079  limsupres  46133  limsupresuz2  46137  limsupequzlem  46150  supcnvlimsup  46168  limsupgtlem  46205  liminfresuz2  46215  cncfmptssg  46299  cncfuni  46314  icccncfext  46315  dvresntr  46346  dvbdfbdioolem1  46356  dvdmsscn  46364  dvnxpaek  46370  dvnprodlem2  46375  stoweidlem59  46487  fourierdlem20  46555  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem52  46586  fourierdlem58  46592  fourierdlem64  46598  fourierdlem73  46607  fourierdlem76  46610  fourierdlem80  46614  fourierdlem84  46618  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  fourierdlem113  46647  etransclem18  46680  ioorrnopnlem  46732  salincl  46752  intsal  46758  fsumlesge0  46805  sge0cl  46809  sge0supre  46817  sge0less  46820  sge0split  46837  sge0seq  46874  caragensspw  46937  omessre  46938  caragendifcl  46942  caratheodorylem1  46954  0ome  46957  omess0  46962  caragencmpl  46963  hoissrrn  46977  hoicvrrex  46984  ovnlecvr  46986  ovnsslelem  46988  ovnssle  46989  ovnsubaddlem1  46998  hoissrrn2  47006  hoidmv1lelem1  47019  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem4  47026  ovnlecvr2  47038  voncmpl  47049  hspmbl  47057  opnvonmbllem1  47060  ovolval5lem2  47081  ovolval5lem3  47082  vonioolem1  47108  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  issmflem  47155  cnfsmf  47168  incsmflem  47169  smfsssmf  47171  smfadd  47193  decsmflem  47194  smflim  47205  smfres  47218  smfmul  47223  smfpimbor1lem1  47226  smfco  47230  smfsuplem1  47239  smfsuplem3  47241  smflimsuplem1  47248  smflimsuplem4  47251  smflimsuplem7  47254  nndivides2  47832  cnneiima  49392  seposep  49401  iscnrm3rlem4  49418  iscnrm3llem1  49424  lubsscl  49435  glbsscl  49436  toplatglb  49476  setrecsss  50176  elpglem1  50186