Theorem sstrd 4005

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

Syntax hints:   → wi 4   ⊆ wss 3962

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

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

This theorem is referenced by:  sstrid  4006  sstrdi  4007  rabssrabd  4092  ssdif2d  4157  uniintsn  4989  funss  6586  fssxp  6763  knatar  7376  tfisi  7879  suppssov1  8220  suppssov2  8221  suppssfv  8225  tposss  8250  frrlem8  8316  tfrlem1  8414  omwordri  8608  oewordri  8628  oeeui  8638  oaabs2  8685  omopthlem1  8695  ecinxp  8830  sbthlem1  9121  dffi2  9460  hartogslem1  9579  cantnfcl  9704  cantnflt  9709  cantnfp1lem3  9717  cantnflem3  9728  cnfcom  9737  cnfcom3lem  9740  ttrcltr  9753  rankssb  9885  tskwe  9987  dfac12lem2  10182  dfac12lem3  10183  cfflb  10296  cfcof  10311  ssfin2  10357  hsmexlem4  10466  ttukeylem6  10551  ttukeylem7  10552  fpwwe2lem1  10668  fpwwe2lem7  10674  fpwwe2lem10  10677  fpwwe2lem11  10678  canthnumlem  10685  canthwelem  10687  canthwe  10688  canthp1lem2  10690  pwfseqlem5  10700  wunex2  10775  tsktrss  10798  inttsk  10811  uzwo3  12982  supicc  13537  supiccub  13538  supicclub  13539  ssfzunsnext  13605  seqsplit  14072  seqf1olem2a  14077  seqz  14087  swrdval2  14680  trrelssd  15008  rtrclreclem4  15096  sumss  15756  qshash  15859  incexc  15869  incexc2  15870  prodss  15979  rpnnen2lem11  16256  vdwlem1  17014  ramub1lem1  17059  imasaddvallem  17575  imasvscaf  17585  mrerintcl  17641  ismred2  17647  mremre  17648  mrcuni  17665  mressmrcd  17671  submrc  17672  mrissmrid  17685  mreexexlem2d  17689  isacs2  17697  isacs1i  17701  invss  17808  ssctr  17872  funcres2b  17947  isacs3lem  18599  acsfiindd  18610  acsmapd  18611  acsmap2d  18612  tsrdir  18661  subsubmgm  18735  subsubm  18841  gsumwspan  18871  subsubg  19179  subgint  19180  cntzidss  19370  symggen  19502  pmtrdifellem1  19508  pmtrdifellem2  19509  pgpssslw  19646  lsmless1x  19676  lsmless2x  19677  lsmless12  19694  subglsm  19705  gsumval3lem2  19938  gsumzaddlem  19953  gsumzadd  19954  gsum2d  20004  dmdprdd  20033  dprdfeq0  20056  dprdspan  20061  dprdres  20062  dprdss  20063  dprdz  20064  subgdmdprd  20068  subgdprd  20069  dprdsn  20070  dprd2dlem1  20075  dprd2da  20076  dmdprdsplit2lem  20079  dprdsplit  20082  pgpfac1lem2  20109  pgpfac1lem3  20111  pgpfac1lem5  20113  subsubrng  20579  subsubrg  20614  subdrgint  20820  lspss  20999  lspun  21002  lsslsp  21030  lsslspOLD  21031  lmhmlsp  21065  lsmelval2  21101  lsmssspx  21104  lsppratlem2  21167  lsppratlem3  21168  lsppratlem4  21169  lbsextlem2  21178  lbsextlem3  21179  ocvlsp  21711  cssmre  21728  obselocv  21765  obslbs  21767  aspss  21914  mhpaddcl  22172  mhpinvcl  22173  mhpvscacl  22175  psdmullem  22186  toponmre  23116  neiint  23127  neiss  23132  lpss  23165  lpss3  23167  restopnb  23198  restfpw  23202  neitr  23203  restcls  23204  restntr  23205  restlp  23206  ordtbas  23215  pnfnei  23243  mnfnei  23244  iscnp4  23286  cnclsi  23295  isreg2  23400  discmp  23421  cmpcld  23425  uncmp  23426  sscmp  23428  hauscmplem  23429  cmpfi  23431  iunconnlem  23450  clsconn  23453  2ndcctbss  23478  restnlly  23505  llyrest  23508  nllyrest  23509  llyidm  23511  nllyidm  23512  cldllycmp  23518  dislly  23520  comppfsc  23555  llycmpkgen2  23573  ptbasfi  23604  txnlly  23660  txcmplem1  23664  tx1stc  23673  xkococnlem  23682  qtopval2  23719  basqtop  23734  tgqtop  23735  qtoprest  23740  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  fsubbas  23890  fgabs  23902  fbasrn  23907  trfil2  23910  trfg  23914  isufil2  23931  trufil  23933  ssufl  23941  ufileu  23942  filufint  23943  fmfnfmlem4  23980  fmfnfm  23981  flimss2  23995  flimss1  23996  fclsfnflim  24050  flimfnfcls  24051  fclscmp  24053  cnpfcfi  24063  alexsubALT  24074  clssubg  24132  clsnsg  24133  tsmsres  24167  ustexsym  24239  ustex2sym  24240  ustex3sym  24241  ustneism  24247  trust  24253  utoptop  24258  restutopopn  24262  utop2nei  24274  utopreg  24276  cfiluweak  24319  neipcfilu  24320  blssps  24449  blss  24450  blcld  24533  blsscls  24535  met1stc  24549  met2ndci  24550  metust  24586  cfilucfil  24587  restmetu  24598  tgqioo  24835  xrsblre  24846  reconnlem2  24862  xrge0gsumle  24868  xrge0tsms  24869  rescncf  24936  cnmpopc  24968  cnheibor  25000  cnllycmp  25001  lebnum  25009  phtpycn  25028  cfilfcls  25321  iscmet3lem2  25339  cmetss  25363  cncmet  25369  bcthlem4  25374  bcth3  25378  rrxcph  25439  rrxmetlem  25454  minveclem4a  25477  minveclem4  25479  ivthicc  25506  ovollb  25527  ovollb2lem  25536  ovollb2  25537  nulmbl2  25584  ioorcl2  25620  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  opnmbllem  25649  volcn  25654  volivth  25655  mbfeqalem1  25689  itg10a  25759  mbfi1fseqlem4  25767  ditgcl  25907  ditgswap  25908  ditgsplitlem  25909  limcflf  25930  limcres  25935  dvbss  25950  dvbsss  25951  perfdvf  25952  dvreslem  25958  dvres2lem  25959  dvres3  25962  dvmptresicc  25965  dvcnp  25968  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  dvnff  25973  dvn2bss  25980  dvnres  25981  cpnord  25985  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvnfre  26004  dvmptres2  26014  dvmptntr  26023  dvcnvlem  26028  dvcnv  26029  dvferm1lem  26036  dvferm2lem  26038  dvlip  26046  dvlipcn  26047  dvlip2  26048  c1liplem1  26049  dvgt0lem1  26055  lhop1lem  26066  lhop  26069  dvcnvrelem1  26070  dvcnvrelem2  26071  dvcnvre  26072  dvfsumle  26074  dvfsumleOLD  26075  dvfsumge  26076  dvfsumabs  26077  ftc1lem1  26090  ftc1lem2  26091  ftc1a  26092  ftc1lem4  26094  ftc2ditglem  26100  itgsubstlem  26103  ig1peu  26228  ig1pdvds  26233  taylfvallem1  26412  tayl0  26417  taylply2  26423  taylply2OLD  26424  taylply  26425  dvtaylp  26426  dvntaylp  26427  dvntaylp0  26428  taylthlem1  26429  ulmdvlem1  26457  ulmdvlem3  26459  psercn  26484  pserdvlem2  26486  abelth  26499  xrlimcnp  27025  lgamucov  27095  wilthlem2  27126  sqff1o  27239  chtublem  27269  pntlemq  27659  pntlemf  27663  sssslt1  27854  sssslt2  27855  scutbdaybnd  27874  scutbdaybnd2  27875  cofss  27978  coiniss  27979  tglineintmo  28664  ttgcontlem1  28913  pthdlem1  29798  shintcli  31357  shub1  31410  mdslmd1lem1  32353  mdexchi  32363  chirredlem1  32418  mdsymlem5  32435  sumdmdii  32443  sumdmdlem2  32447  fnpreimac  32687  fsuppinisegfi  32701  xrsupssd  32769  xrge0infssd  32771  swrdrn3  32924  swrdf1  32925  swrdrndisj  32926  pwrssmgc  32974  xrge0tsmsd  33047  elrgspnlem4  33234  fldgenss  33297  fldgenssp  33299  linds2eq  33388  elrspunidl  33435  ssdifidllem  33463  ssdifidlprm  33465  mxidlprm  33477  ssmxidllem  33480  ssmxidl  33481  qsdrnglem2  33503  rprmdvdsprod  33541  resssra  33616  lsssra  33617  lbsdiflsp0  33653  dimkerim  33654  fedgmullem1  33656  fedgmullem2  33657  fedgmul  33658  dimlssid  33659  constr01  33746  constrmon  33748  smatrcl  33756  locfinreflem  33800  cmpcref  33810  zarclsun  33830  zarclsiin  33831  zarclssn  33833  zarcmplem  33841  pnfneige0  33911  esum2d  34073  insiga  34117  sssigagen2  34126  dynkin  34147  dya2iocnei  34263  omsmon  34279  carsgclctunlem1  34298  carsggect  34299  omsmeas  34304  ftc2re  34591  fdvneggt  34593  fdvnegge  34595  reprsuc  34608  reprss  34610  reprlt  34612  reprinfz1  34615  logdivsqrle  34643  hgt750lemb  34649  bnj906  34922  bnj1020  34957  bnj1137  34987  bnj1408  35028  bnj1452  35044  erdszelem7  35181  erdszelem8  35182  erdsze2lem1  35187  connpconn  35219  cvmliftmolem1  35265  cvmlift2lem1  35286  cvmlift2lem9  35295  cvmlift2lem10  35296  cvmlift3lem6  35308  cvmlift3lem7  35309  satfsschain  35348  ss2mcls  35552  neibastop2lem  36342  fnemeet2  36349  fnejoin1  36350  ontgval  36413  unbdqndv1  36490  opnmbllem0  37642  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  sstotbnd2  37760  heiborlem1  37797  heiborlem8  37804  intidl  38015  lsmsat  38989  lssats  38993  lpssat  38994  lssatle  38996  lssat  38997  lsatcvatlem  39030  paddss12  39801  paddasslem17  39818  pmodlem1  39828  pmod1i  39830  pmodl42N  39833  elpcliN  39875  pclfinN  39882  polcon3N  39899  polcon2N  39901  paddunN  39909  pclfinclN  39932  poml5N  39936  osumcllem1N  39938  osumcllem2N  39939  osumcllem3N  39940  pl42lem2N  39962  pl42lem4N  39964  cdlemn5pre  41182  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord5b  41241  dochss  41347  dochdmj1  41372  djhsumss  41389  djhunssN  41391  dochexmidlem2  41443  lclkrslem1  41519  lclkrslem2  41520  lcfrlem2  41525  aks4d1p4  42060  aks4d1p5  42061  aks4d1p7  42064  aks4d1p8  42068  aks6d1c2  42111  sticksstones1  42127  unitscyglem5  42180  prjcrv0  42619  elrfi  42681  ismrcd1  42685  istopclsd  42687  mrefg2  42694  aomclem2  43043  aomclem6  43047  hbtlem6  43117  hbt  43118  oege2  43296  cantnftermord  43309  omabs2  43321  tfsconcat0b  43335  naddgeoa  43383  naddwordnexlem0  43385  naddwordnexlem1  43386  dfno2  43417  mptrcllem  43602  dfrcl2  43663  relexp0a  43705  trclimalb2  43715  frege81d  43736  k0004ss2  44141  imo72b2lem2  44156  imo72b2  44161  uzwo4  44992  ssin0  44994  ixpssmapc  45012  ssinc  45026  ssdec  45027  supxrre3  45274  uzfissfz  45275  ssuzfz  45298  supminfxr  45413  inficc  45486  ressiocsup  45506  ressioosup  45507  ressiooinf  45509  limccog  45575  limclner  45606  limsupres  45660  limsupresuz2  45664  limsupequzlem  45677  supcnvlimsup  45695  limsupgtlem  45732  liminfresuz2  45742  cncfmptssg  45826  cncfuni  45841  icccncfext  45842  dvresntr  45873  dvbdfbdioolem1  45883  dvdmsscn  45891  dvnxpaek  45897  dvnprodlem2  45902  stoweidlem59  46014  fourierdlem20  46082  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem52  46113  fourierdlem58  46119  fourierdlem64  46125  fourierdlem73  46134  fourierdlem76  46137  fourierdlem80  46141  fourierdlem84  46145  fourierdlem93  46154  fourierdlem103  46164  fourierdlem104  46165  fourierdlem113  46174  etransclem18  46207  ioorrnopnlem  46259  salincl  46279  intsal  46285  fsumlesge0  46332  sge0cl  46336  sge0supre  46344  sge0less  46347  sge0split  46364  sge0seq  46401  caragensspw  46464  omessre  46465  caragendifcl  46469  caratheodorylem1  46481  0ome  46484  omess0  46489  caragencmpl  46490  hoicvr  46503  hoissrrn  46504  hoicvrrex  46511  ovnlecvr  46513  ovnsslelem  46515  ovnssle  46516  ovnsubaddlem1  46525  hoissrrn2  46533  hoidmv1lelem1  46546  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem4  46553  ovnlecvr2  46565  voncmpl  46576  hspmbl  46584  opnvonmbllem1  46587  ovolval5lem2  46608  ovolval5lem3  46609  vonioolem1  46635  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  issmflem  46682  cnfsmf  46695  incsmflem  46696  smfsssmf  46698  smfadd  46720  decsmflem  46721  smflim  46732  smfres  46745  smfmul  46750  smfpimbor1lem1  46753  smfco  46757  smfsuplem1  46766  smfsuplem3  46768  smflimsuplem1  46775  smflimsuplem4  46778  smflimsuplem7  46781  cnneiima  48712  seposep  48721  iscnrm3rlem4  48739  iscnrm3llem1  48745  lubsscl  48756  glbsscl  48757  toplatglb  48789  setrecsss  48931  elpglem1  48941