Theorem sstrd 3949

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

Syntax hints:   → wi 4   ⊆ wss 3907

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3924

This theorem is referenced by:  sstrid  3950  sstrdi  3951  rabssrabd  4039  ssdif2d  4104  uniintsn  4946  funss  6544  fssxp  6723  knatar  7345  tfisi  7843  suppssov1  8181  suppssov2  8182  suppssfv  8186  tposss  8211  frrlem8  8278  tfrlem1  8350  omwordri  8545  oewordri  8566  oeeui  8576  oaabs2  8623  omopthlem1  8633  ecinxp  8778  sbthlem1  9063  dffi2  9371  hartogslem1  9492  cantnfcl  9624  cantnflt  9629  cantnfp1lem3  9637  cantnflem3  9648  cnfcom  9657  cnfcom3lem  9660  ttrcltr  9673  rankssb  9808  tskwe  9924  dfac12lem2  10116  dfac12lem3  10117  cfflb  10231  cfcof  10246  ssfin2  10292  hsmexlem4  10401  ttukeylem6  10486  ttukeylem7  10487  fpwwe2lem1  10604  fpwwe2lem7  10610  fpwwe2lem10  10613  fpwwe2lem11  10614  canthnumlem  10621  canthwelem  10623  canthwe  10624  canthp1lem2  10626  pwfseqlem5  10636  wunex2  10711  tsktrss  10734  inttsk  10747  uzwo3  12958  xrsupssd  13350  supicc  13519  supiccub  13520  supicclub  13521  ssfzunsnext  13588  seqsplit  14062  seqf1olem2a  14067  seqz  14077  swrdval2  14674  trrelssd  15000  rtrclreclem4  15088  sumss  15765  qshash  15869  incexc  15881  incexc2  15882  prodss  15991  rpnnen2lem11  16270  vdwlem1  17031  ramub1lem1  17076  imasaddvallem  17573  imasvscaf  17583  mrerintcl  17639  ismred2  17645  mremre  17646  mrcuni  17667  mressmrcd  17673  submrc  17674  mrissmrid  17687  mreexexlem2d  17691  isacs2  17699  isacs1i  17703  invss  17808  ssctr  17872  funcres2b  17944  isacs3lem  18588  acsfiindd  18599  acsmapd  18600  acsmap2d  18601  tsrdir  18650  subsubmgm  18758  subsubm  18865  gsumwspan  18895  subsubg  19207  subgint  19208  cntzidss  19401  symggen  19531  pmtrdifellem1  19537  pmtrdifellem2  19538  pgpssslw  19675  lsmless1x  19705  lsmless2x  19706  lsmless12  19723  subglsm  19734  gsumval3lem2  19967  gsumzaddlem  19982  gsumzadd  19983  gsum2d  20033  dmdprdd  20062  dprdfeq0  20085  dprdspan  20090  dprdres  20091  dprdss  20092  dprdz  20093  subgdmdprd  20097  subgdprd  20098  dprdsn  20099  dprd2dlem1  20104  dprd2da  20105  dmdprdsplit2lem  20108  dprdsplit  20111  pgpfac1lem2  20138  pgpfac1lem3  20140  pgpfac1lem5  20142  subsubrng  20639  subsubrg  20674  subdrgint  20875  lspss  21074  lspun  21077  lsslsp  21105  lmhmlsp  21139  lsmelval2  21175  lsmssspx  21178  lsppratlem2  21241  lsppratlem3  21242  lsppratlem4  21243  lbsextlem2  21252  lbsextlem3  21253  ssdifidllem  21444  ssdifidlprm  21446  ocvlsp  21786  cssmre  21803  obselocv  21838  obslbs  21840  aspss  21986  mhpaddcl  22274  mhpinvcl  22275  mhpvscacl  22277  psdmullem  22288  toponmre  23211  neiint  23222  neiss  23227  lpss  23260  lpss3  23262  restopnb  23293  restfpw  23297  neitr  23298  restcls  23299  restntr  23300  restlp  23301  ordtbas  23310  pnfnei  23338  mnfnei  23339  iscnp4  23381  cnclsi  23390  isreg2  23495  discmp  23516  cmpcld  23520  uncmp  23521  sscmp  23523  hauscmplem  23524  cmpfi  23526  iunconnlem  23545  clsconn  23548  2ndcctbss  23573  restnlly  23600  llyrest  23603  nllyrest  23604  llyidm  23606  nllyidm  23607  cldllycmp  23613  dislly  23615  comppfsc  23650  llycmpkgen2  23668  ptbasfi  23699  txnlly  23755  txcmplem1  23759  tx1stc  23768  xkococnlem  23777  qtopval2  23814  basqtop  23829  tgqtop  23830  qtoprest  23835  kqreglem1  23859  kqreglem2  23860  kqnrmlem1  23861  kqnrmlem2  23862  fsubbas  23985  fgabs  23997  fbasrn  24002  trfil2  24005  trfg  24009  isufil2  24026  trufil  24028  ssufl  24036  ufileu  24037  filufint  24038  fmfnfmlem4  24075  fmfnfm  24076  flimss2  24090  flimss1  24091  fclsfnflim  24145  flimfnfcls  24146  fclscmp  24148  cnpfcfi  24158  alexsubALT  24169  clssubg  24227  clsnsg  24228  tsmsres  24262  ustexsym  24334  ustex2sym  24335  ustex3sym  24336  ustneism  24342  trust  24347  utoptop  24352  restutopopn  24356  utop2nei  24368  utopreg  24370  cfiluweak  24412  neipcfilu  24413  blssps  24542  blss  24543  blcld  24623  blsscls  24625  met1stc  24639  met2ndci  24640  metust  24676  cfilucfil  24677  restmetu  24688  tgqioo  24918  xrsblre  24930  reconnlem2  24946  xrge0gsumle  24952  xrge0tsms  24953  rescncf  25017  cnmpopc  25048  cnheibor  25075  cnllycmp  25076  lebnum  25084  phtpycn  25103  cfilfcls  25394  iscmet3lem2  25412  cmetss  25436  cncmet  25442  bcthlem4  25447  bcth3  25451  rrxcph  25512  rrxmetlem  25527  minveclem4a  25550  minveclem4  25552  ivthicc  25578  ovollb  25599  ovollb2lem  25608  ovollb2  25609  nulmbl2  25656  ioorcl2  25692  uniioombllem3  25705  uniioombllem4  25706  uniioombllem5  25707  opnmbllem  25721  volcn  25726  volivth  25727  mbfeqalem1  25761  itg10a  25830  mbfi1fseqlem4  25838  ditgcl  25978  ditgswap  25979  ditgsplitlem  25980  limcflf  26001  limcres  26006  dvbss  26021  dvbsss  26022  perfdvf  26023  dvreslem  26029  dvres2lem  26030  dvres3  26033  dvmptresicc  26036  dvcnp  26039  dvcnp2  26040  dvcn  26041  dvnff  26043  dvn2bss  26050  dvnres  26051  cpnord  26055  dvaddbr  26058  dvmulbr  26059  dvcobr  26066  dvnfre  26072  dvmptres2  26082  dvmptntr  26091  dvcnvlem  26096  dvcnv  26097  dvferm1lem  26104  dvferm2lem  26106  dvlip  26113  dvlipcn  26114  dvlip2  26115  c1liplem1  26116  dvgt0lem1  26122  lhop1lem  26133  lhop  26136  dvcnvrelem1  26137  dvcnvrelem2  26138  dvcnvre  26139  dvfsumle  26141  dvfsumge  26142  dvfsumabs  26143  ftc1lem1  26155  ftc1lem2  26156  ftc1a  26157  ftc1lem4  26159  ftc2ditglem  26165  itgsubstlem  26168  ig1peu  26293  ig1pdvds  26298  taylfvallem1  26478  tayl0  26483  taylply2  26489  taylply  26490  dvtaylp  26491  dvntaylp  26492  dvntaylp0  26493  taylthlem1  26494  ulmdvlem1  26521  ulmdvlem3  26523  psercn  26547  pserdvlem2  26549  abelth  26562  xrlimcnp  27091  lgamucov  27160  wilthlem2  27191  sqff1o  27304  chtublem  27333  pntlemq  27723  pntlemf  27727  ssslts1  27924  ssslts2  27925  cutbdaybnd  27946  cutbdaybnd2  27947  eqcuts3  27955  cofss  28081  coiniss  28082  bdaypw2bnd  28616  bdayfinbndlem1  28618  z12bdaylem2  28622  tglineintmo  28869  ttgcontlem1  29143  pthdlem1  30024  shintcli  31590  shub1  31643  mdslmd1lem1  32586  mdexchi  32596  chirredlem1  32651  mdsymlem5  32668  sumdmdii  32676  sumdmdlem2  32680  fnpreimac  32927  fsuppinisegfi  32944  xrge0infssd  33018  swrdrn3  33188  swrdf1  33189  swrdrndisj  33190  pwrssmgc  33233  xrge0tsmsd  33306  elrgspnlem4  33478  elrgspnsubrunlem1  33480  elrgspnsubrunlem2  33481  fldgenss  33552  fldgenssp  33554  linds2eq  33610  elrspunidl  33652  mxidlprm  33670  ssmxidllem  33673  ssmxidl  33674  qsdrnglem2  33695  rprmdvdsprod  33741  ressply1evls1  33772  resssra  33894  lsssra  33895  exsslsb  33904  lbsdiflsp0  33933  dimkerim  33934  fedgmullem1  33936  fedgmullem2  33937  fedgmul  33938  dimlssid  33939  fldextrspunlsplem  33980  fldextrspunlsp  33981  fldextrspunlem1  33982  fldextrspundgdvdslem  33987  fldextrspundgdvds  33988  constr01  34049  constrmon  34051  constrextdg2lem  34055  constrfiss  34058  smatrcl  34103  locfinreflem  34147  cmpcref  34157  zarclsun  34177  zarclsiin  34178  zarclssn  34180  zarcmplem  34188  pnfneige0  34258  esum2d  34400  insiga  34444  sssigagen2  34453  dynkin  34474  dya2iocnei  34589  omsmon  34605  carsgclctunlem1  34624  carsggect  34625  omsmeas  34630  ftc2re  34902  fdvneggt  34904  fdvnegge  34906  reprsuc  34919  reprss  34921  reprlt  34923  reprinfz1  34926  logdivsqrle  34954  hgt750lemb  34960  bnj906  35235  bnj1020  35270  bnj1137  35300  bnj1408  35341  bnj1452  35357  rankval4b  35408  fineqvnttrclselem2  35430  erdszelem7  35560  erdszelem8  35561  erdsze2lem1  35566  connpconn  35598  cvmliftmolem1  35644  cvmlift2lem1  35665  cvmlift2lem9  35674  cvmlift2lem10  35675  cvmlift3lem6  35687  cvmlift3lem7  35688  satfsschain  35727  ss2mcls  35931  neibastop2lem  36733  fnemeet2  36740  fnejoin1  36741  ontgval  36804  ttcmin  36869  unbdqndv1  36959  opnmbllem0  38167  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  sstotbnd2  38285  heiborlem1  38322  heiborlem8  38329  intidl  38540  lsmsat  39644  lssats  39648  lpssat  39649  lssatle  39651  lssat  39652  lsatcvatlem  39685  paddss12  40455  paddasslem17  40472  pmodlem1  40482  pmod1i  40484  pmodl42N  40487  elpcliN  40529  pclfinN  40536  polcon3N  40553  polcon2N  40555  paddunN  40563  pclfinclN  40586  poml5N  40590  osumcllem1N  40592  osumcllem2N  40593  osumcllem3N  40594  pl42lem2N  40616  pl42lem4N  40618  cdlemn5pre  41836  dihord1  41854  dihord2a  41855  dihord2b  41856  dihord5b  41895  dochss  42001  dochdmj1  42026  djhsumss  42043  djhunssN  42045  dochexmidlem2  42097  lclkrslem1  42173  lclkrslem2  42174  lcfrlem2  42179  aks4d1p4  42708  aks4d1p5  42709  aks4d1p7  42712  aks4d1p8  42716  aks6d1c2  42759  sticksstones1  42775  unitscyglem5  42828  prjcrv0  43227  elrfi  43287  ismrcd1  43291  istopclsd  43293  mrefg2  43300  aomclem2  43644  aomclem6  43648  hbtlem6  43718  hbt  43719  oege2  43896  cantnftermord  43909  omabs2  43921  tfsconcat0b  43935  naddgeoa  43983  naddwordnexlem0  43985  naddwordnexlem1  43986  dfno2  44016  mptrcllem  44201  dfrcl2  44262  relexp0a  44304  trclimalb2  44314  frege81d  44335  k0004ss2  44740  imo72b2lem2  44755  imo72b2  44760  uzwo4  45631  ssin0  45633  ixpssmapc  45651  ssinc  45663  ssdec  45664  supxrre3  45899  uzfissfz  45900  ssuzfz  45923  supminfxr  46036  inficc  46108  ressiocsup  46128  ressioosup  46129  ressiooinf  46131  limccog  46194  limclner  46223  limsupres  46277  limsupresuz2  46281  limsupequzlem  46294  supcnvlimsup  46312  limsupgtlem  46349  liminfresuz2  46359  cncfmptssg  46443  icccncfext  46459  dvresntr  46490  dvbdfbdioolem1  46500  dvdmsscn  46508  dvnxpaek  46514  dvnprodlem2  46519  stoweidlem59  46631  fourierdlem20  46699  fourierdlem42  46721  fourierdlem48  46726  fourierdlem49  46727  fourierdlem52  46730  fourierdlem58  46736  fourierdlem64  46742  fourierdlem73  46751  fourierdlem76  46754  fourierdlem80  46758  fourierdlem84  46762  fourierdlem93  46771  fourierdlem103  46781  fourierdlem104  46782  fourierdlem113  46791  etransclem18  46824  ioorrnopnlem  46876  salincl  46896  intsal  46902  fsumlesge0  46949  sge0cl  46953  sge0supre  46961  sge0less  46964  sge0split  46981  sge0seq  47018  caragensspw  47081  omessre  47082  caragendifcl  47086  caratheodorylem1  47098  0ome  47101  omess0  47106  caragencmpl  47107  hoissrrn  47121  hoicvrrex  47128  ovnlecvr  47130  ovnsslelem  47132  ovnssle  47133  ovnsubaddlem1  47142  hoissrrn2  47150  hoidmv1lelem1  47163  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem4  47170  ovnlecvr2  47182  voncmpl  47193  hspmbl  47201  opnvonmbllem1  47204  ovolval5lem2  47225  ovolval5lem3  47226  vonioolem1  47252  pimdecfgtioc  47287  pimincfltioc  47288  pimdecfgtioo  47289  pimincfltioo  47290  issmflem  47299  cnfsmf  47312  incsmflem  47313  smfsssmf  47315  smfadd  47337  decsmflem  47338  smflim  47349  smfres  47362  smfmul  47367  smfpimbor1lem1  47370  smfco  47374  smfsuplem1  47383  smfsuplem3  47385  smflimsuplem1  47392  smflimsuplem4  47395  smflimsuplem7  47398  nndivides2  47976  cnneiima  49546  seposep  49555  iscnrm3rlem4  49572  iscnrm3llem1  49578  lubsscl  49589  glbsscl  49590  toplatglb  49630  setrecsss  50330  elpglem1  50340