Theorem sstrd 3993

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

Syntax hints:   → wi 4   ⊆ wss 3949

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sstrid  3994  sstrdi  3995  rabssrabd  4082  ssdif2d  4144  uniintsn  4992  funss  6568  fssxp  6746  knatar  7354  tfisi  7848  suppssov1  8183  suppssfv  8187  tposss  8212  frrlem8  8278  tfrlem1  8376  omwordri  8572  oewordri  8592  oeeui  8602  oaabs2  8648  omopthlem1  8658  ecinxp  8786  sbthlem1  9083  dffi2  9418  hartogslem1  9537  cantnfcl  9662  cantnflt  9667  cantnfp1lem3  9675  cantnflem3  9686  cnfcom  9695  cnfcom3lem  9698  ttrcltr  9711  rankssb  9843  tskwe  9945  dfac12lem2  10139  dfac12lem3  10140  cfflb  10254  cfcof  10269  ssfin2  10315  hsmexlem4  10424  ttukeylem6  10509  ttukeylem7  10510  fpwwe2lem1  10626  fpwwe2lem7  10632  fpwwe2lem10  10635  fpwwe2lem11  10636  canthnumlem  10643  canthwelem  10645  canthwe  10646  canthp1lem2  10648  pwfseqlem5  10658  wunex2  10733  tsktrss  10756  inttsk  10769  uzwo3  12927  supicc  13478  supiccub  13479  supicclub  13480  ssfzunsnext  13546  seqsplit  14001  seqf1olem2a  14006  seqz  14016  swrdval2  14596  trrelssd  14920  rtrclreclem4  15008  sumss  15670  qshash  15773  incexc  15783  incexc2  15784  prodss  15891  rpnnen2lem11  16167  vdwlem1  16914  ramub1lem1  16959  imasaddvallem  17475  imasvscaf  17485  mrerintcl  17541  ismred2  17547  mremre  17548  mrcuni  17565  mressmrcd  17571  submrc  17572  mrissmrid  17585  mreexexlem2d  17589  isacs2  17597  isacs1i  17601  invss  17708  ssctr  17772  funcres2b  17847  isacs3lem  18495  acsfiindd  18506  acsmapd  18507  acsmap2d  18508  tsrdir  18557  subsubm  18697  gsumwspan  18727  subsubg  19029  subgint  19030  cntzidss  19204  symggen  19338  pmtrdifellem1  19344  pmtrdifellem2  19345  pgpssslw  19482  lsmless1x  19512  lsmless2x  19513  lsmless12  19530  subglsm  19541  gsumval3lem2  19774  gsumzaddlem  19789  gsumzadd  19790  gsum2d  19840  dmdprdd  19869  dprdfeq0  19892  dprdspan  19897  dprdres  19898  dprdss  19899  dprdz  19900  subgdmdprd  19904  subgdprd  19905  dprdsn  19906  dprd2dlem1  19911  dprd2da  19912  dmdprdsplit2lem  19915  dprdsplit  19918  pgpfac1lem2  19945  pgpfac1lem3  19947  pgpfac1lem5  19949  subsubrg  20345  subdrgint  20419  lspss  20595  lspun  20598  lsslsp  20626  lmhmlsp  20660  lsmelval2  20696  lsmssspx  20699  lsppratlem2  20761  lsppratlem3  20762  lsppratlem4  20763  lbsextlem2  20772  lbsextlem3  20773  ocvlsp  21229  cssmre  21246  obselocv  21283  obslbs  21285  aspss  21431  mhpaddcl  21694  mhpinvcl  21695  mhpvscacl  21697  toponmre  22597  neiint  22608  neiss  22613  lpss  22646  lpss3  22648  restopnb  22679  restfpw  22683  neitr  22684  restcls  22685  restntr  22686  restlp  22687  ordtbas  22696  pnfnei  22724  mnfnei  22725  iscnp4  22767  cnclsi  22776  isreg2  22881  discmp  22902  cmpcld  22906  uncmp  22907  sscmp  22909  hauscmplem  22910  cmpfi  22912  iunconnlem  22931  clsconn  22934  2ndcctbss  22959  restnlly  22986  llyrest  22989  nllyrest  22990  llyidm  22992  nllyidm  22993  cldllycmp  22999  dislly  23001  comppfsc  23036  llycmpkgen2  23054  ptbasfi  23085  txnlly  23141  txcmplem1  23145  tx1stc  23154  xkococnlem  23163  qtopval2  23200  basqtop  23215  tgqtop  23216  qtoprest  23221  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  fsubbas  23371  fgabs  23383  fbasrn  23388  trfil2  23391  trfg  23395  isufil2  23412  trufil  23414  ssufl  23422  ufileu  23423  filufint  23424  fmfnfmlem4  23461  fmfnfm  23462  flimss2  23476  flimss1  23477  fclsfnflim  23531  flimfnfcls  23532  fclscmp  23534  cnpfcfi  23544  alexsubALT  23555  clssubg  23613  clsnsg  23614  tsmsres  23648  ustexsym  23720  ustex2sym  23721  ustex3sym  23722  ustneism  23728  trust  23734  utoptop  23739  restutopopn  23743  utop2nei  23755  utopreg  23757  cfiluweak  23800  neipcfilu  23801  blssps  23930  blss  23931  blcld  24014  blsscls  24016  met1stc  24030  met2ndci  24031  metust  24067  cfilucfil  24068  restmetu  24079  tgqioo  24316  xrsblre  24327  reconnlem2  24343  xrge0gsumle  24349  xrge0tsms  24350  rescncf  24413  cnmpopc  24444  cnheibor  24471  cnllycmp  24472  lebnum  24480  phtpycn  24499  cfilfcls  24791  iscmet3lem2  24809  cmetss  24833  cncmet  24839  bcthlem4  24844  bcth3  24848  rrxcph  24909  rrxmetlem  24924  minveclem4a  24947  minveclem4  24949  ivthicc  24975  ovollb  24996  ovollb2lem  25005  ovollb2  25006  nulmbl2  25053  ioorcl2  25089  uniioombllem3  25102  uniioombllem4  25103  uniioombllem5  25104  opnmbllem  25118  volcn  25123  volivth  25124  mbfeqalem1  25158  itg10a  25228  mbfi1fseqlem4  25236  ditgcl  25375  ditgswap  25376  ditgsplitlem  25377  limcflf  25398  limcres  25403  dvbss  25418  dvbsss  25419  perfdvf  25420  dvreslem  25426  dvres2lem  25427  dvres3  25430  dvmptresicc  25433  dvcnp  25436  dvcnp2  25437  dvcn  25438  dvnff  25440  dvn2bss  25447  dvnres  25448  cpnord  25452  dvaddbr  25455  dvmulbr  25456  dvcobr  25463  dvnfre  25469  dvmptres2  25479  dvmptntr  25488  dvcnvlem  25493  dvcnv  25494  dvferm1lem  25501  dvferm2lem  25503  dvlip  25510  dvlipcn  25511  dvlip2  25512  c1liplem1  25513  dvgt0lem1  25519  lhop1lem  25530  lhop  25533  dvcnvrelem1  25534  dvcnvrelem2  25535  dvcnvre  25536  dvfsumle  25538  dvfsumge  25539  dvfsumabs  25540  ftc1lem1  25552  ftc1lem2  25553  ftc1a  25554  ftc1lem4  25556  ftc2ditglem  25562  itgsubstlem  25565  ig1peu  25689  ig1pdvds  25694  taylfvallem1  25869  tayl0  25874  taylply2  25880  taylply  25881  dvtaylp  25882  dvntaylp  25883  dvntaylp0  25884  taylthlem1  25885  ulmdvlem1  25912  ulmdvlem3  25914  psercn  25938  pserdvlem2  25940  abelth  25953  xrlimcnp  26473  lgamucov  26542  wilthlem2  26573  sqff1o  26686  chtublem  26714  pntlemq  27104  pntlemf  27108  sssslt1  27296  sssslt2  27297  scutbdaybnd  27316  scutbdaybnd2  27317  cofss  27417  coiniss  27418  tglineintmo  27893  ttgcontlem1  28142  pthdlem1  29023  shintcli  30582  shub1  30635  mdslmd1lem1  31578  mdexchi  31588  chirredlem1  31643  mdsymlem5  31660  sumdmdii  31668  sumdmdlem2  31672  fnpreimac  31896  fsuppinisegfi  31909  xrsupssd  31972  xrge0infssd  31974  swrdrn3  32119  swrdf1  32120  swrdrndisj  32121  pwrssmgc  32170  xrge0tsmsd  32209  fldgenss  32406  fldgenssp  32408  linds2eq  32497  elrspunidl  32546  mxidlprm  32586  ssmxidllem  32589  ssmxidl  32590  qsdrnglem2  32610  lbsdiflsp0  32711  dimkerim  32712  fedgmullem1  32714  fedgmullem2  32715  fedgmul  32716  smatrcl  32776  locfinreflem  32820  cmpcref  32830  zarclsun  32850  zarclsiin  32851  zarclssn  32853  zarcmplem  32861  pnfneige0  32931  esum2d  33091  insiga  33135  sssigagen2  33144  dynkin  33165  dya2iocnei  33281  omsmon  33297  carsgclctunlem1  33316  carsggect  33317  omsmeas  33322  ftc2re  33610  fdvneggt  33612  fdvnegge  33614  reprsuc  33627  reprss  33629  reprlt  33631  reprinfz1  33634  logdivsqrle  33662  hgt750lemb  33668  bnj906  33941  bnj1020  33976  bnj1137  34006  bnj1408  34047  bnj1452  34063  erdszelem7  34188  erdszelem8  34189  erdsze2lem1  34194  connpconn  34226  cvmliftmolem1  34272  cvmlift2lem1  34293  cvmlift2lem9  34302  cvmlift2lem10  34303  cvmlift3lem6  34315  cvmlift3lem7  34316  satfsschain  34355  ss2mcls  34559  gg-dvcnp2  35174  gg-dvmulbr  35175  gg-dvcobr  35176  gg-dvfsumle  35182  neibastop2lem  35245  fnemeet2  35252  fnejoin1  35253  ontgval  35316  unbdqndv1  35384  opnmbllem0  36524  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  sstotbnd2  36642  heiborlem1  36679  heiborlem8  36686  intidl  36897  lsmsat  37878  lssats  37882  lpssat  37883  lssatle  37885  lssat  37886  lsatcvatlem  37919  paddss12  38690  paddasslem17  38707  pmodlem1  38717  pmod1i  38719  pmodl42N  38722  elpcliN  38764  pclfinN  38771  polcon3N  38788  polcon2N  38790  paddunN  38798  pclfinclN  38821  poml5N  38825  osumcllem1N  38827  osumcllem2N  38828  osumcllem3N  38829  pl42lem2N  38851  pl42lem4N  38853  cdlemn5pre  40071  dihord1  40089  dihord2a  40090  dihord2b  40091  dihord5b  40130  dochss  40236  dochdmj1  40261  djhsumss  40278  djhunssN  40280  dochexmidlem2  40332  lclkrslem1  40408  lclkrslem2  40409  lcfrlem2  40414  aks4d1p4  40944  aks4d1p5  40945  aks4d1p7  40948  aks4d1p8  40952  sticksstones1  40962  prjcrv0  41375  elrfi  41432  ismrcd1  41436  istopclsd  41438  mrefg2  41445  aomclem2  41797  aomclem6  41801  hbtlem6  41871  hbt  41872  oege2  42057  cantnftermord  42070  omabs2  42082  tfsconcat0b  42096  naddgeoa  42145  naddwordnexlem0  42147  naddwordnexlem1  42148  dfno2  42179  mptrcllem  42364  dfrcl2  42425  relexp0a  42467  trclimalb2  42477  frege81d  42498  k0004ss2  42903  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2  42924  uzwo4  43740  ssin0  43742  ixpssmapc  43761  ssinc  43776  ssdec  43777  supxrre3  44035  uzfissfz  44036  ssuzfz  44059  supminfxr  44174  inficc  44247  ressiocsup  44267  ressioosup  44268  ressiooinf  44270  limccog  44336  limclner  44367  limsupres  44421  limsupresuz2  44425  limsupequzlem  44438  limsupvaluz2  44454  supcnvlimsup  44456  limsupgtlem  44493  liminfresuz2  44503  cncfmptssg  44587  cncfuni  44602  icccncfext  44603  dvresntr  44634  dvbdfbdioolem1  44644  dvdmsscn  44652  dvnxpaek  44658  dvnprodlem2  44663  stoweidlem59  44775  fourierdlem20  44843  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem52  44874  fourierdlem58  44880  fourierdlem64  44886  fourierdlem73  44895  fourierdlem76  44898  fourierdlem80  44902  fourierdlem84  44906  fourierdlem93  44915  fourierdlem103  44925  fourierdlem104  44926  fourierdlem113  44935  etransclem18  44968  ioorrnopnlem  45020  salincl  45040  intsal  45046  fsumlesge0  45093  sge0cl  45097  sge0supre  45105  sge0less  45108  sge0split  45125  sge0seq  45162  caragensspw  45225  omessre  45226  caragendifcl  45230  caratheodorylem1  45242  0ome  45245  omess0  45250  caragencmpl  45251  hoicvr  45264  hoissrrn  45265  hoicvrrex  45272  ovnlecvr  45274  ovnsslelem  45276  ovnssle  45277  ovnsubaddlem1  45286  hoissrrn2  45294  hoidmv1lelem1  45307  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem4  45314  ovnlecvr2  45326  voncmpl  45337  hspmbl  45345  opnvonmbllem1  45348  ovolval5lem2  45369  ovolval5lem3  45370  vonioolem1  45396  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  issmflem  45443  cnfsmf  45456  incsmflem  45457  smfsssmf  45459  smfadd  45481  decsmflem  45482  smflim  45493  smfres  45506  smfmul  45511  smfpimbor1lem1  45514  smfco  45518  smfsuplem1  45527  smfsuplem3  45529  smflimsuplem1  45536  smflimsuplem4  45539  smflimsuplem7  45542  subsubmgm  46567  subsubrng  46742  cnneiima  47549  seposep  47558  iscnrm3rlem4  47576  iscnrm3llem1  47582  lubsscl  47593  glbsscl  47594  toplatglb  47626  setrecsss  47746  elpglem1  47756