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

Syntax hints:   → wi 4   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sstrid  3933  sstrdi  3934  rabssrabd  4017  ssdif2d  4079  uniintsn  4919  funss  6460  fssxp  6637  knatar  7237  tfisi  7714  suppssov1  8023  suppssfv  8027  tposss  8052  frrlem8  8118  tfrlem1  8216  omwordri  8412  oewordri  8432  oeeui  8442  oaabs2  8488  omopthlem1  8498  ecinxp  8590  sbthlem1  8879  dffi2  9191  hartogslem1  9310  cantnfcl  9434  cantnflt  9439  cantnfp1lem3  9447  cantnflem3  9458  cnfcom  9467  cnfcom3lem  9470  ttrcltr  9483  rankssb  9615  tskwe  9717  dfac12lem2  9909  dfac12lem3  9910  cfflb  10024  cfcof  10039  ssfin2  10085  hsmexlem4  10194  ttukeylem6  10279  ttukeylem7  10280  fpwwe2lem1  10396  fpwwe2lem7  10402  fpwwe2lem10  10405  fpwwe2lem11  10406  canthnumlem  10413  canthwelem  10415  canthwe  10416  canthp1lem2  10418  pwfseqlem5  10428  wunex2  10503  tsktrss  10526  inttsk  10539  uzwo3  12692  supicc  13242  supiccub  13243  supicclub  13244  ssfzunsnext  13310  seqsplit  13765  seqf1olem2a  13770  seqz  13780  swrdval2  14368  trrelssd  14693  rtrclreclem4  14781  sumss  15445  qshash  15548  incexc  15558  incexc2  15559  prodss  15666  rpnnen2lem11  15942  vdwlem1  16691  ramub1lem1  16736  imasaddvallem  17249  imasvscaf  17259  mrerintcl  17315  ismred2  17321  mremre  17322  mrcuni  17339  mressmrcd  17345  submrc  17346  mrissmrid  17359  mreexexlem2d  17363  isacs2  17371  isacs1i  17375  invss  17482  ssctr  17546  funcres2b  17621  isacs3lem  18269  acsfiindd  18280  acsmapd  18281  acsmap2d  18282  tsrdir  18331  subsubm  18464  gsumwspan  18494  subsubg  18787  subgint  18788  cntzidss  18953  symggen  19087  pmtrdifellem1  19093  pmtrdifellem2  19094  pgpssslw  19228  lsmless1x  19258  lsmless2x  19259  lsmless12  19276  subglsm  19288  gsumval3lem2  19516  gsumzaddlem  19531  gsumzadd  19532  gsum2d  19582  dmdprdd  19611  dprdfeq0  19634  dprdspan  19639  dprdres  19640  dprdss  19641  dprdz  19642  subgdmdprd  19646  subgdprd  19647  dprdsn  19648  dprd2dlem1  19653  dprd2da  19654  dmdprdsplit2lem  19657  dprdsplit  19660  pgpfac1lem2  19687  pgpfac1lem3  19689  pgpfac1lem5  19691  subsubrg  20059  subdrgint  20080  lspss  20255  lspun  20258  lsslsp  20286  lmhmlsp  20320  lsmelval2  20356  lsmssspx  20359  lsppratlem2  20419  lsppratlem3  20420  lsppratlem4  20421  lbsextlem2  20430  lbsextlem3  20431  ocvlsp  20890  cssmre  20907  obselocv  20944  obslbs  20946  aspss  21090  mhpaddcl  21350  mhpinvcl  21351  mhpvscacl  21353  toponmre  22253  neiint  22264  neiss  22269  lpss  22302  lpss3  22304  restopnb  22335  restfpw  22339  neitr  22340  restcls  22341  restntr  22342  restlp  22343  ordtbas  22352  pnfnei  22380  mnfnei  22381  iscnp4  22423  cnclsi  22432  isreg2  22537  discmp  22558  cmpcld  22562  uncmp  22563  sscmp  22565  hauscmplem  22566  cmpfi  22568  iunconnlem  22587  clsconn  22590  2ndcctbss  22615  restnlly  22642  llyrest  22645  nllyrest  22646  llyidm  22648  nllyidm  22649  cldllycmp  22655  dislly  22657  comppfsc  22692  llycmpkgen2  22710  ptbasfi  22741  txnlly  22797  txcmplem1  22801  tx1stc  22810  xkococnlem  22819  qtopval2  22856  basqtop  22871  tgqtop  22872  qtoprest  22877  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  fsubbas  23027  fgabs  23039  fbasrn  23044  trfil2  23047  trfg  23051  isufil2  23068  trufil  23070  ssufl  23078  ufileu  23079  filufint  23080  fmfnfmlem4  23117  fmfnfm  23118  flimss2  23132  flimss1  23133  fclsfnflim  23187  flimfnfcls  23188  fclscmp  23190  cnpfcfi  23200  alexsubALT  23211  clssubg  23269  clsnsg  23270  tsmsres  23304  ustexsym  23376  ustex2sym  23377  ustex3sym  23378  ustneism  23384  trust  23390  utoptop  23395  restutopopn  23399  utop2nei  23411  utopreg  23413  cfiluweak  23456  neipcfilu  23457  blssps  23586  blss  23587  blcld  23670  blsscls  23672  met1stc  23686  met2ndci  23687  metust  23723  cfilucfil  23724  restmetu  23735  tgqioo  23972  xrsblre  23983  reconnlem2  23999  xrge0gsumle  24005  xrge0tsms  24006  rescncf  24069  cnmpopc  24100  cnheibor  24127  cnllycmp  24128  lebnum  24136  phtpycn  24155  cfilfcls  24447  iscmet3lem2  24465  cmetss  24489  cncmet  24495  bcthlem4  24500  bcth3  24504  rrxcph  24565  rrxmetlem  24580  minveclem4a  24603  minveclem4  24605  ivthicc  24631  ovollb  24652  ovollb2lem  24661  ovollb2  24662  nulmbl2  24709  ioorcl2  24745  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  opnmbllem  24774  volcn  24779  volivth  24780  mbfeqalem1  24814  itg10a  24884  mbfi1fseqlem4  24892  ditgcl  25031  ditgswap  25032  ditgsplitlem  25033  limcflf  25054  limcres  25059  dvbss  25074  dvbsss  25075  perfdvf  25076  dvreslem  25082  dvres2lem  25083  dvres3  25086  dvmptresicc  25089  dvcnp  25092  dvcnp2  25093  dvcn  25094  dvnff  25096  dvn2bss  25103  dvnres  25104  cpnord  25108  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  dvnfre  25125  dvmptres2  25135  dvmptntr  25144  dvcnvlem  25149  dvcnv  25150  dvferm1lem  25157  dvferm2lem  25159  dvlip  25166  dvlipcn  25167  dvlip2  25168  c1liplem1  25169  dvgt0lem1  25175  lhop1lem  25186  lhop  25189  dvcnvrelem1  25190  dvcnvrelem2  25191  dvcnvre  25192  dvfsumle  25194  dvfsumge  25195  dvfsumabs  25196  ftc1lem1  25208  ftc1lem2  25209  ftc1a  25210  ftc1lem4  25212  ftc2ditglem  25218  itgsubstlem  25221  ig1peu  25345  ig1pdvds  25350  taylfvallem1  25525  tayl0  25530  taylply2  25536  taylply  25537  dvtaylp  25538  dvntaylp  25539  dvntaylp0  25540  taylthlem1  25541  ulmdvlem1  25568  ulmdvlem3  25570  psercn  25594  pserdvlem2  25596  abelth  25609  xrlimcnp  26127  lgamucov  26196  wilthlem2  26227  sqff1o  26340  chtublem  26368  pntlemq  26758  pntlemf  26762  tglineintmo  27012  ttgcontlem1  27261  pthdlem1  28143  shintcli  29700  shub1  29753  mdslmd1lem1  30696  mdexchi  30706  chirredlem1  30761  mdsymlem5  30778  sumdmdii  30786  sumdmdlem2  30790  fnpreimac  31017  fsuppinisegfi  31030  xrsupssd  31091  xrge0infssd  31093  swrdrn3  31236  swrdf1  31237  swrdrndisj  31238  pwrssmgc  31287  xrge0tsmsd  31326  linds2eq  31584  elrspunidl  31615  mxidlprm  31649  ssmxidllem  31650  ssmxidl  31651  lbsdiflsp0  31716  dimkerim  31717  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  smatrcl  31755  locfinreflem  31799  cmpcref  31809  zarclsun  31829  zarclsiin  31830  zarclssn  31832  zarcmplem  31840  pnfneige0  31910  esum2d  32070  insiga  32114  sssigagen2  32123  dynkin  32144  dya2iocnei  32258  omsmon  32274  carsgclctunlem1  32293  carsggect  32294  omsmeas  32299  ftc2re  32587  fdvneggt  32589  fdvnegge  32591  reprsuc  32604  reprss  32606  reprlt  32608  reprinfz1  32611  logdivsqrle  32639  hgt750lemb  32645  bnj906  32919  bnj1020  32954  bnj1137  32984  bnj1408  33025  bnj1452  33041  erdszelem7  33168  erdszelem8  33169  erdsze2lem1  33174  connpconn  33206  cvmliftmolem1  33252  cvmlift2lem1  33273  cvmlift2lem9  33282  cvmlift2lem10  33283  cvmlift3lem6  33295  cvmlift3lem7  33296  satfsschain  33335  ss2mcls  33539  sssslt1  33998  sssslt2  33999  scutbdaybnd  34018  scutbdaybnd2  34019  neibastop2lem  34558  fnemeet2  34565  fnejoin1  34566  ontgval  34629  unbdqndv1  34697  opnmbllem0  35822  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  sstotbnd2  35941  heiborlem1  35978  heiborlem8  35985  intidl  36196  lsmsat  37029  lssats  37033  lpssat  37034  lssatle  37036  lssat  37037  lsatcvatlem  37070  paddss12  37840  paddasslem17  37857  pmodlem1  37867  pmod1i  37869  pmodl42N  37872  elpcliN  37914  pclfinN  37921  polcon3N  37938  polcon2N  37940  paddunN  37948  pclfinclN  37971  poml5N  37975  osumcllem1N  37977  osumcllem2N  37978  osumcllem3N  37979  pl42lem2N  38001  pl42lem4N  38003  cdlemn5pre  39221  dihord1  39239  dihord2a  39240  dihord2b  39241  dihord5b  39280  dochss  39386  dochdmj1  39411  djhsumss  39428  djhunssN  39430  dochexmidlem2  39482  lclkrslem1  39558  lclkrslem2  39559  lcfrlem2  39564  aks4d1p4  40094  aks4d1p5  40095  aks4d1p7  40098  aks4d1p8  40102  sticksstones1  40109  elrfi  40523  ismrcd1  40527  istopclsd  40529  mrefg2  40536  aomclem2  40887  aomclem6  40891  hbtlem6  40961  hbt  40962  mptrcllem  41228  dfrcl2  41289  relexp0a  41331  trclimalb2  41341  frege81d  41362  k0004ss2  41769  imo72b2lem0  41783  imo72b2lem2  41785  imo72b2  41790  uzwo4  42608  ssin0  42610  ixpssmapc  42629  ssinc  42644  ssdec  42645  supxrre3  42871  uzfissfz  42872  ssuzfz  42895  supminfxr  43011  inficc  43079  ressiocsup  43099  ressioosup  43100  ressiooinf  43102  limccog  43168  limclner  43199  limsupres  43253  limsupresuz2  43257  limsupequzlem  43270  limsupvaluz2  43286  supcnvlimsup  43288  limsupgtlem  43325  liminfresuz2  43335  cncfmptssg  43419  cncfuni  43434  icccncfext  43435  dvresntr  43466  dvbdfbdioolem1  43476  dvdmsscn  43484  dvnxpaek  43490  dvnprodlem2  43495  stoweidlem59  43607  fourierdlem20  43675  fourierdlem42  43697  fourierdlem48  43702  fourierdlem49  43703  fourierdlem52  43706  fourierdlem58  43712  fourierdlem64  43718  fourierdlem73  43727  fourierdlem76  43730  fourierdlem80  43734  fourierdlem84  43738  fourierdlem93  43747  fourierdlem103  43757  fourierdlem104  43758  fourierdlem113  43767  etransclem18  43800  ioorrnopnlem  43852  salincl  43871  intsal  43876  fsumlesge0  43922  sge0cl  43926  sge0supre  43934  sge0less  43937  sge0split  43954  sge0seq  43991  caragensspw  44054  omessre  44055  caragendifcl  44059  caratheodorylem1  44071  0ome  44074  omess0  44079  caragencmpl  44080  hoicvr  44093  hoissrrn  44094  hoicvrrex  44101  ovnlecvr  44103  ovnsslelem  44105  ovnssle  44106  ovnsubaddlem1  44115  hoissrrn2  44123  hoidmv1lelem1  44136  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem4  44143  ovnlecvr2  44155  voncmpl  44166  hspmbl  44174  opnvonmbllem1  44177  ovolval5lem2  44198  ovolval5lem3  44199  vonioolem1  44225  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  issmflem  44272  cnfsmf  44285  incsmflem  44286  smfsssmf  44288  smfadd  44310  decsmflem  44311  smflim  44322  smfres  44335  smfmul  44340  smfpimbor1lem1  44343  smfco  44347  smfsuplem1  44355  smfsuplem3  44357  smflimsuplem1  44364  smflimsuplem4  44367  smflimsuplem7  44370  subsubmgm  45362  cnneiima  46221  seposep  46230  iscnrm3rlem4  46248  iscnrm3llem1  46254  lubsscl  46265  glbsscl  46266  toplatglb  46298  setrecsss  46417  elpglem1  46427