Theorem sstrd 4019

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

Syntax hints:   → wi 4   ⊆ wss 3976

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

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

This theorem is referenced by:  sstrid  4020  sstrdi  4021  rabssrabd  4106  ssdif2d  4171  uniintsn  5009  funss  6597  fssxp  6775  knatar  7393  tfisi  7896  suppssov1  8238  suppssov2  8239  suppssfv  8243  tposss  8268  frrlem8  8334  tfrlem1  8432  omwordri  8628  oewordri  8648  oeeui  8658  oaabs2  8705  omopthlem1  8715  ecinxp  8850  sbthlem1  9149  dffi2  9492  hartogslem1  9611  cantnfcl  9736  cantnflt  9741  cantnfp1lem3  9749  cantnflem3  9760  cnfcom  9769  cnfcom3lem  9772  ttrcltr  9785  rankssb  9917  tskwe  10019  dfac12lem2  10214  dfac12lem3  10215  cfflb  10328  cfcof  10343  ssfin2  10389  hsmexlem4  10498  ttukeylem6  10583  ttukeylem7  10584  fpwwe2lem1  10700  fpwwe2lem7  10706  fpwwe2lem10  10709  fpwwe2lem11  10710  canthnumlem  10717  canthwelem  10719  canthwe  10720  canthp1lem2  10722  pwfseqlem5  10732  wunex2  10807  tsktrss  10830  inttsk  10843  uzwo3  13008  supicc  13561  supiccub  13562  supicclub  13563  ssfzunsnext  13629  seqsplit  14086  seqf1olem2a  14091  seqz  14101  swrdval2  14694  trrelssd  15022  rtrclreclem4  15110  sumss  15772  qshash  15875  incexc  15885  incexc2  15886  prodss  15995  rpnnen2lem11  16272  vdwlem1  17028  ramub1lem1  17073  imasaddvallem  17589  imasvscaf  17599  mrerintcl  17655  ismred2  17661  mremre  17662  mrcuni  17679  mressmrcd  17685  submrc  17686  mrissmrid  17699  mreexexlem2d  17703  isacs2  17711  isacs1i  17715  invss  17822  ssctr  17886  funcres2b  17961  isacs3lem  18612  acsfiindd  18623  acsmapd  18624  acsmap2d  18625  tsrdir  18674  subsubmgm  18748  subsubm  18851  gsumwspan  18881  subsubg  19189  subgint  19190  cntzidss  19380  symggen  19512  pmtrdifellem1  19518  pmtrdifellem2  19519  pgpssslw  19656  lsmless1x  19686  lsmless2x  19687  lsmless12  19704  subglsm  19715  gsumval3lem2  19948  gsumzaddlem  19963  gsumzadd  19964  gsum2d  20014  dmdprdd  20043  dprdfeq0  20066  dprdspan  20071  dprdres  20072  dprdss  20073  dprdz  20074  subgdmdprd  20078  subgdprd  20079  dprdsn  20080  dprd2dlem1  20085  dprd2da  20086  dmdprdsplit2lem  20089  dprdsplit  20092  pgpfac1lem2  20119  pgpfac1lem3  20121  pgpfac1lem5  20123  subsubrng  20589  subsubrg  20626  subdrgint  20826  lspss  21005  lspun  21008  lsslsp  21036  lsslspOLD  21037  lmhmlsp  21071  lsmelval2  21107  lsmssspx  21110  lsppratlem2  21173  lsppratlem3  21174  lsppratlem4  21175  lbsextlem2  21184  lbsextlem3  21185  ocvlsp  21717  cssmre  21734  obselocv  21771  obslbs  21773  aspss  21920  mhpaddcl  22178  mhpinvcl  22179  mhpvscacl  22181  psdmullem  22192  toponmre  23122  neiint  23133  neiss  23138  lpss  23171  lpss3  23173  restopnb  23204  restfpw  23208  neitr  23209  restcls  23210  restntr  23211  restlp  23212  ordtbas  23221  pnfnei  23249  mnfnei  23250  iscnp4  23292  cnclsi  23301  isreg2  23406  discmp  23427  cmpcld  23431  uncmp  23432  sscmp  23434  hauscmplem  23435  cmpfi  23437  iunconnlem  23456  clsconn  23459  2ndcctbss  23484  restnlly  23511  llyrest  23514  nllyrest  23515  llyidm  23517  nllyidm  23518  cldllycmp  23524  dislly  23526  comppfsc  23561  llycmpkgen2  23579  ptbasfi  23610  txnlly  23666  txcmplem1  23670  tx1stc  23679  xkococnlem  23688  qtopval2  23725  basqtop  23740  tgqtop  23741  qtoprest  23746  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  fsubbas  23896  fgabs  23908  fbasrn  23913  trfil2  23916  trfg  23920  isufil2  23937  trufil  23939  ssufl  23947  ufileu  23948  filufint  23949  fmfnfmlem4  23986  fmfnfm  23987  flimss2  24001  flimss1  24002  fclsfnflim  24056  flimfnfcls  24057  fclscmp  24059  cnpfcfi  24069  alexsubALT  24080  clssubg  24138  clsnsg  24139  tsmsres  24173  ustexsym  24245  ustex2sym  24246  ustex3sym  24247  ustneism  24253  trust  24259  utoptop  24264  restutopopn  24268  utop2nei  24280  utopreg  24282  cfiluweak  24325  neipcfilu  24326  blssps  24455  blss  24456  blcld  24539  blsscls  24541  met1stc  24555  met2ndci  24556  metust  24592  cfilucfil  24593  restmetu  24604  tgqioo  24841  xrsblre  24852  reconnlem2  24868  xrge0gsumle  24874  xrge0tsms  24875  rescncf  24942  cnmpopc  24974  cnheibor  25006  cnllycmp  25007  lebnum  25015  phtpycn  25034  cfilfcls  25327  iscmet3lem2  25345  cmetss  25369  cncmet  25375  bcthlem4  25380  bcth3  25384  rrxcph  25445  rrxmetlem  25460  minveclem4a  25483  minveclem4  25485  ivthicc  25512  ovollb  25533  ovollb2lem  25542  ovollb2  25543  nulmbl2  25590  ioorcl2  25626  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  opnmbllem  25655  volcn  25660  volivth  25661  mbfeqalem1  25695  itg10a  25765  mbfi1fseqlem4  25773  ditgcl  25913  ditgswap  25914  ditgsplitlem  25915  limcflf  25936  limcres  25941  dvbss  25956  dvbsss  25957  perfdvf  25958  dvreslem  25964  dvres2lem  25965  dvres3  25968  dvmptresicc  25971  dvcnp  25974  dvcnp2  25975  dvcnp2OLD  25976  dvcn  25977  dvnff  25979  dvn2bss  25986  dvnres  25987  cpnord  25991  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvnfre  26010  dvmptres2  26020  dvmptntr  26029  dvcnvlem  26034  dvcnv  26035  dvferm1lem  26042  dvferm2lem  26044  dvlip  26052  dvlipcn  26053  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  lhop1lem  26072  lhop  26075  dvcnvrelem1  26076  dvcnvrelem2  26077  dvcnvre  26078  dvfsumle  26080  dvfsumleOLD  26081  dvfsumge  26082  dvfsumabs  26083  ftc1lem1  26096  ftc1lem2  26097  ftc1a  26098  ftc1lem4  26100  ftc2ditglem  26106  itgsubstlem  26109  ig1peu  26234  ig1pdvds  26239  taylfvallem1  26416  tayl0  26421  taylply2  26427  taylply2OLD  26428  taylply  26429  dvtaylp  26430  dvntaylp  26431  dvntaylp0  26432  taylthlem1  26433  ulmdvlem1  26461  ulmdvlem3  26463  psercn  26488  pserdvlem2  26490  abelth  26503  xrlimcnp  27029  lgamucov  27099  wilthlem2  27130  sqff1o  27243  chtublem  27273  pntlemq  27663  pntlemf  27667  sssslt1  27858  sssslt2  27859  scutbdaybnd  27878  scutbdaybnd2  27879  cofss  27982  coiniss  27983  tglineintmo  28668  ttgcontlem1  28917  pthdlem1  29802  shintcli  31361  shub1  31414  mdslmd1lem1  32357  mdexchi  32367  chirredlem1  32422  mdsymlem5  32439  sumdmdii  32447  sumdmdlem2  32451  fnpreimac  32689  fsuppinisegfi  32699  xrsupssd  32766  xrge0infssd  32768  swrdrn3  32922  swrdf1  32923  swrdrndisj  32924  pwrssmgc  32973  xrge0tsmsd  33041  fldgenss  33283  fldgenssp  33285  linds2eq  33374  elrspunidl  33421  ssdifidllem  33449  ssdifidlprm  33451  mxidlprm  33463  ssmxidllem  33466  ssmxidl  33467  qsdrnglem2  33489  rprmdvdsprod  33527  resssra  33602  lsssra  33603  lbsdiflsp0  33639  dimkerim  33640  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  dimlssid  33645  constr01  33732  constrmon  33734  smatrcl  33742  locfinreflem  33786  cmpcref  33796  zarclsun  33816  zarclsiin  33817  zarclssn  33819  zarcmplem  33827  pnfneige0  33897  esum2d  34057  insiga  34101  sssigagen2  34110  dynkin  34131  dya2iocnei  34247  omsmon  34263  carsgclctunlem1  34282  carsggect  34283  omsmeas  34288  ftc2re  34575  fdvneggt  34577  fdvnegge  34579  reprsuc  34592  reprss  34594  reprlt  34596  reprinfz1  34599  logdivsqrle  34627  hgt750lemb  34633  bnj906  34906  bnj1020  34941  bnj1137  34971  bnj1408  35012  bnj1452  35028  erdszelem7  35165  erdszelem8  35166  erdsze2lem1  35171  connpconn  35203  cvmliftmolem1  35249  cvmlift2lem1  35270  cvmlift2lem9  35279  cvmlift2lem10  35280  cvmlift3lem6  35292  cvmlift3lem7  35293  satfsschain  35332  ss2mcls  35536  neibastop2lem  36326  fnemeet2  36333  fnejoin1  36334  ontgval  36397  unbdqndv1  36474  opnmbllem0  37616  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  sstotbnd2  37734  heiborlem1  37771  heiborlem8  37778  intidl  37989  lsmsat  38964  lssats  38968  lpssat  38969  lssatle  38971  lssat  38972  lsatcvatlem  39005  paddss12  39776  paddasslem17  39793  pmodlem1  39803  pmod1i  39805  pmodl42N  39808  elpcliN  39850  pclfinN  39857  polcon3N  39874  polcon2N  39876  paddunN  39884  pclfinclN  39907  poml5N  39911  osumcllem1N  39913  osumcllem2N  39914  osumcllem3N  39915  pl42lem2N  39937  pl42lem4N  39939  cdlemn5pre  41157  dihord1  41175  dihord2a  41176  dihord2b  41177  dihord5b  41216  dochss  41322  dochdmj1  41347  djhsumss  41364  djhunssN  41366  dochexmidlem2  41418  lclkrslem1  41494  lclkrslem2  41495  lcfrlem2  41500  aks4d1p4  42036  aks4d1p5  42037  aks4d1p7  42040  aks4d1p8  42044  aks6d1c2  42087  sticksstones1  42103  unitscyglem5  42156  prjcrv0  42588  elrfi  42650  ismrcd1  42654  istopclsd  42656  mrefg2  42663  aomclem2  43012  aomclem6  43016  hbtlem6  43086  hbt  43087  oege2  43269  cantnftermord  43282  omabs2  43294  tfsconcat0b  43308  naddgeoa  43356  naddwordnexlem0  43358  naddwordnexlem1  43359  dfno2  43390  mptrcllem  43575  dfrcl2  43636  relexp0a  43678  trclimalb2  43688  frege81d  43709  k0004ss2  44114  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2  44134  uzwo4  44955  ssin0  44957  ixpssmapc  44975  ssinc  44989  ssdec  44990  supxrre3  45240  uzfissfz  45241  ssuzfz  45264  supminfxr  45379  inficc  45452  ressiocsup  45472  ressioosup  45473  ressiooinf  45475  limccog  45541  limclner  45572  limsupres  45626  limsupresuz2  45630  limsupequzlem  45643  limsupvaluz2  45659  supcnvlimsup  45661  limsupgtlem  45698  liminfresuz2  45708  cncfmptssg  45792  cncfuni  45807  icccncfext  45808  dvresntr  45839  dvbdfbdioolem1  45849  dvdmsscn  45857  dvnxpaek  45863  dvnprodlem2  45868  stoweidlem59  45980  fourierdlem20  46048  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem52  46079  fourierdlem58  46085  fourierdlem64  46091  fourierdlem73  46100  fourierdlem76  46103  fourierdlem80  46107  fourierdlem84  46111  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  fourierdlem113  46140  etransclem18  46173  ioorrnopnlem  46225  salincl  46245  intsal  46251  fsumlesge0  46298  sge0cl  46302  sge0supre  46310  sge0less  46313  sge0split  46330  sge0seq  46367  caragensspw  46430  omessre  46431  caragendifcl  46435  caratheodorylem1  46447  0ome  46450  omess0  46455  caragencmpl  46456  hoicvr  46469  hoissrrn  46470  hoicvrrex  46477  ovnlecvr  46479  ovnsslelem  46481  ovnssle  46482  ovnsubaddlem1  46491  hoissrrn2  46499  hoidmv1lelem1  46512  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem4  46519  ovnlecvr2  46531  voncmpl  46542  hspmbl  46550  opnvonmbllem1  46553  ovolval5lem2  46574  ovolval5lem3  46575  vonioolem1  46601  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  issmflem  46648  cnfsmf  46661  incsmflem  46662  smfsssmf  46664  smfadd  46686  decsmflem  46687  smflim  46698  smfres  46711  smfmul  46716  smfpimbor1lem1  46719  smfco  46723  smfsuplem1  46732  smfsuplem3  46734  smflimsuplem1  46741  smflimsuplem4  46744  smflimsuplem7  46747  cnneiima  48596  seposep  48605  iscnrm3rlem4  48623  iscnrm3llem1  48629  lubsscl  48640  glbsscl  48641  toplatglb  48673  setrecsss  48793  elpglem1  48803