Theorem sstrd 3960

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

Syntax hints:   → wi 4   ⊆ wss 3917

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

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

This theorem is referenced by:  sstrid  3961  sstrdi  3962  rabssrabd  4049  ssdif2d  4114  uniintsn  4952  funss  6538  fssxp  6718  knatar  7335  tfisi  7838  suppssov1  8179  suppssov2  8180  suppssfv  8184  tposss  8209  frrlem8  8275  tfrlem1  8347  omwordri  8539  oewordri  8559  oeeui  8569  oaabs2  8616  omopthlem1  8626  ecinxp  8768  sbthlem1  9057  dffi2  9381  hartogslem1  9502  cantnfcl  9627  cantnflt  9632  cantnfp1lem3  9640  cantnflem3  9651  cnfcom  9660  cnfcom3lem  9663  ttrcltr  9676  rankssb  9808  tskwe  9910  dfac12lem2  10105  dfac12lem3  10106  cfflb  10219  cfcof  10234  ssfin2  10280  hsmexlem4  10389  ttukeylem6  10474  ttukeylem7  10475  fpwwe2lem1  10591  fpwwe2lem7  10597  fpwwe2lem10  10600  fpwwe2lem11  10601  canthnumlem  10608  canthwelem  10610  canthwe  10611  canthp1lem2  10613  pwfseqlem5  10623  wunex2  10698  tsktrss  10721  inttsk  10734  uzwo3  12909  xrsupssd  13300  supicc  13469  supiccub  13470  supicclub  13471  ssfzunsnext  13537  seqsplit  14007  seqf1olem2a  14012  seqz  14022  swrdval2  14618  trrelssd  14946  rtrclreclem4  15034  sumss  15697  qshash  15800  incexc  15810  incexc2  15811  prodss  15920  rpnnen2lem11  16199  vdwlem1  16959  ramub1lem1  17004  imasaddvallem  17499  imasvscaf  17509  mrerintcl  17565  ismred2  17571  mremre  17572  mrcuni  17589  mressmrcd  17595  submrc  17596  mrissmrid  17609  mreexexlem2d  17613  isacs2  17621  isacs1i  17625  invss  17730  ssctr  17794  funcres2b  17866  isacs3lem  18508  acsfiindd  18519  acsmapd  18520  acsmap2d  18521  tsrdir  18570  subsubmgm  18644  subsubm  18750  gsumwspan  18780  subsubg  19088  subgint  19089  cntzidss  19279  symggen  19407  pmtrdifellem1  19413  pmtrdifellem2  19414  pgpssslw  19551  lsmless1x  19581  lsmless2x  19582  lsmless12  19599  subglsm  19610  gsumval3lem2  19843  gsumzaddlem  19858  gsumzadd  19859  gsum2d  19909  dmdprdd  19938  dprdfeq0  19961  dprdspan  19966  dprdres  19967  dprdss  19968  dprdz  19969  subgdmdprd  19973  subgdprd  19974  dprdsn  19975  dprd2dlem1  19980  dprd2da  19981  dmdprdsplit2lem  19984  dprdsplit  19987  pgpfac1lem2  20014  pgpfac1lem3  20016  pgpfac1lem5  20018  subsubrng  20479  subsubrg  20514  subdrgint  20719  lspss  20897  lspun  20900  lsslsp  20928  lsslspOLD  20929  lmhmlsp  20963  lsmelval2  20999  lsmssspx  21002  lsppratlem2  21065  lsppratlem3  21066  lsppratlem4  21067  lbsextlem2  21076  lbsextlem3  21077  ocvlsp  21592  cssmre  21609  obselocv  21644  obslbs  21646  aspss  21793  mhpaddcl  22045  mhpinvcl  22046  mhpvscacl  22048  psdmullem  22059  toponmre  22987  neiint  22998  neiss  23003  lpss  23036  lpss3  23038  restopnb  23069  restfpw  23073  neitr  23074  restcls  23075  restntr  23076  restlp  23077  ordtbas  23086  pnfnei  23114  mnfnei  23115  iscnp4  23157  cnclsi  23166  isreg2  23271  discmp  23292  cmpcld  23296  uncmp  23297  sscmp  23299  hauscmplem  23300  cmpfi  23302  iunconnlem  23321  clsconn  23324  2ndcctbss  23349  restnlly  23376  llyrest  23379  nllyrest  23380  llyidm  23382  nllyidm  23383  cldllycmp  23389  dislly  23391  comppfsc  23426  llycmpkgen2  23444  ptbasfi  23475  txnlly  23531  txcmplem1  23535  tx1stc  23544  xkococnlem  23553  qtopval2  23590  basqtop  23605  tgqtop  23606  qtoprest  23611  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  fsubbas  23761  fgabs  23773  fbasrn  23778  trfil2  23781  trfg  23785  isufil2  23802  trufil  23804  ssufl  23812  ufileu  23813  filufint  23814  fmfnfmlem4  23851  fmfnfm  23852  flimss2  23866  flimss1  23867  fclsfnflim  23921  flimfnfcls  23922  fclscmp  23924  cnpfcfi  23934  alexsubALT  23945  clssubg  24003  clsnsg  24004  tsmsres  24038  ustexsym  24110  ustex2sym  24111  ustex3sym  24112  ustneism  24118  trust  24124  utoptop  24129  restutopopn  24133  utop2nei  24145  utopreg  24147  cfiluweak  24189  neipcfilu  24190  blssps  24319  blss  24320  blcld  24400  blsscls  24402  met1stc  24416  met2ndci  24417  metust  24453  cfilucfil  24454  restmetu  24465  tgqioo  24695  xrsblre  24707  reconnlem2  24723  xrge0gsumle  24729  xrge0tsms  24730  rescncf  24797  cnmpopc  24829  cnheibor  24861  cnllycmp  24862  lebnum  24870  phtpycn  24889  cfilfcls  25181  iscmet3lem2  25199  cmetss  25223  cncmet  25229  bcthlem4  25234  bcth3  25238  rrxcph  25299  rrxmetlem  25314  minveclem4a  25337  minveclem4  25339  ivthicc  25366  ovollb  25387  ovollb2lem  25396  ovollb2  25397  nulmbl2  25444  ioorcl2  25480  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  opnmbllem  25509  volcn  25514  volivth  25515  mbfeqalem1  25549  itg10a  25618  mbfi1fseqlem4  25626  ditgcl  25766  ditgswap  25767  ditgsplitlem  25768  limcflf  25789  limcres  25794  dvbss  25809  dvbsss  25810  perfdvf  25811  dvreslem  25817  dvres2lem  25818  dvres3  25821  dvmptresicc  25824  dvcnp  25827  dvcnp2  25828  dvcnp2OLD  25829  dvcn  25830  dvnff  25832  dvn2bss  25839  dvnres  25840  cpnord  25844  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcobr  25856  dvcobrOLD  25857  dvnfre  25863  dvmptres2  25873  dvmptntr  25882  dvcnvlem  25887  dvcnv  25888  dvferm1lem  25895  dvferm2lem  25897  dvlip  25905  dvlipcn  25906  dvlip2  25907  c1liplem1  25908  dvgt0lem1  25914  lhop1lem  25925  lhop  25928  dvcnvrelem1  25929  dvcnvrelem2  25930  dvcnvre  25931  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvfsumabs  25936  ftc1lem1  25949  ftc1lem2  25950  ftc1a  25951  ftc1lem4  25953  ftc2ditglem  25959  itgsubstlem  25962  ig1peu  26087  ig1pdvds  26092  taylfvallem1  26271  tayl0  26276  taylply2  26282  taylply2OLD  26283  taylply  26284  dvtaylp  26285  dvntaylp  26286  dvntaylp0  26287  taylthlem1  26288  ulmdvlem1  26316  ulmdvlem3  26318  psercn  26343  pserdvlem2  26345  abelth  26358  xrlimcnp  26885  lgamucov  26955  wilthlem2  26986  sqff1o  27099  chtublem  27129  pntlemq  27519  pntlemf  27523  sssslt1  27714  sssslt2  27715  scutbdaybnd  27734  scutbdaybnd2  27735  cofss  27845  coiniss  27846  tglineintmo  28576  ttgcontlem1  28819  pthdlem1  29703  shintcli  31265  shub1  31318  mdslmd1lem1  32261  mdexchi  32271  chirredlem1  32326  mdsymlem5  32343  sumdmdii  32351  sumdmdlem2  32355  fnpreimac  32602  fsuppinisegfi  32617  xrge0infssd  32691  swrdrn3  32884  swrdf1  32885  swrdrndisj  32886  pwrssmgc  32933  xrge0tsmsd  33009  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  fldgenss  33273  fldgenssp  33275  linds2eq  33359  elrspunidl  33406  ssdifidllem  33434  ssdifidlprm  33436  mxidlprm  33448  ssmxidllem  33451  ssmxidl  33452  qsdrnglem2  33474  rprmdvdsprod  33512  ressply1evls1  33541  resssra  33590  lsssra  33591  exsslsb  33599  lbsdiflsp0  33629  dimkerim  33630  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  dimlssid  33635  fldextrspunlsplem  33675  fldextrspunlsp  33676  fldextrspunlem1  33677  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  constr01  33739  constrmon  33741  constrextdg2lem  33745  constrfiss  33748  smatrcl  33793  locfinreflem  33837  cmpcref  33847  zarclsun  33867  zarclsiin  33868  zarclssn  33870  zarcmplem  33878  pnfneige0  33948  esum2d  34090  insiga  34134  sssigagen2  34143  dynkin  34164  dya2iocnei  34280  omsmon  34296  carsgclctunlem1  34315  carsggect  34316  omsmeas  34321  ftc2re  34596  fdvneggt  34598  fdvnegge  34600  reprsuc  34613  reprss  34615  reprlt  34617  reprinfz1  34620  logdivsqrle  34648  hgt750lemb  34654  bnj906  34927  bnj1020  34962  bnj1137  34992  bnj1408  35033  bnj1452  35049  erdszelem7  35191  erdszelem8  35192  erdsze2lem1  35197  connpconn  35229  cvmliftmolem1  35275  cvmlift2lem1  35296  cvmlift2lem9  35305  cvmlift2lem10  35306  cvmlift3lem6  35318  cvmlift3lem7  35319  satfsschain  35358  ss2mcls  35562  neibastop2lem  36355  fnemeet2  36362  fnejoin1  36363  ontgval  36426  unbdqndv1  36503  opnmbllem0  37657  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  sstotbnd2  37775  heiborlem1  37812  heiborlem8  37819  intidl  38030  lsmsat  39008  lssats  39012  lpssat  39013  lssatle  39015  lssat  39016  lsatcvatlem  39049  paddss12  39820  paddasslem17  39837  pmodlem1  39847  pmod1i  39849  pmodl42N  39852  elpcliN  39894  pclfinN  39901  polcon3N  39918  polcon2N  39920  paddunN  39928  pclfinclN  39951  poml5N  39955  osumcllem1N  39957  osumcllem2N  39958  osumcllem3N  39959  pl42lem2N  39981  pl42lem4N  39983  cdlemn5pre  41201  dihord1  41219  dihord2a  41220  dihord2b  41221  dihord5b  41260  dochss  41366  dochdmj1  41391  djhsumss  41408  djhunssN  41410  dochexmidlem2  41462  lclkrslem1  41538  lclkrslem2  41539  lcfrlem2  41544  aks4d1p4  42074  aks4d1p5  42075  aks4d1p7  42078  aks4d1p8  42082  aks6d1c2  42125  sticksstones1  42141  unitscyglem5  42194  prjcrv0  42628  elrfi  42689  ismrcd1  42693  istopclsd  42695  mrefg2  42702  aomclem2  43051  aomclem6  43055  hbtlem6  43125  hbt  43126  oege2  43303  cantnftermord  43316  omabs2  43328  tfsconcat0b  43342  naddgeoa  43390  naddwordnexlem0  43392  naddwordnexlem1  43393  dfno2  43424  mptrcllem  43609  dfrcl2  43670  relexp0a  43712  trclimalb2  43722  frege81d  43743  k0004ss2  44148  imo72b2lem2  44163  imo72b2  44168  uzwo4  45054  ssin0  45056  ixpssmapc  45074  ssinc  45088  ssdec  45089  supxrre3  45328  uzfissfz  45329  ssuzfz  45352  supminfxr  45467  inficc  45539  ressiocsup  45559  ressioosup  45560  ressiooinf  45562  limccog  45625  limclner  45656  limsupres  45710  limsupresuz2  45714  limsupequzlem  45727  supcnvlimsup  45745  limsupgtlem  45782  liminfresuz2  45792  cncfmptssg  45876  cncfuni  45891  icccncfext  45892  dvresntr  45923  dvbdfbdioolem1  45933  dvdmsscn  45941  dvnxpaek  45947  dvnprodlem2  45952  stoweidlem59  46064  fourierdlem20  46132  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem52  46163  fourierdlem58  46169  fourierdlem64  46175  fourierdlem73  46184  fourierdlem76  46187  fourierdlem80  46191  fourierdlem84  46195  fourierdlem93  46204  fourierdlem103  46214  fourierdlem104  46215  fourierdlem113  46224  etransclem18  46257  ioorrnopnlem  46309  salincl  46329  intsal  46335  fsumlesge0  46382  sge0cl  46386  sge0supre  46394  sge0less  46397  sge0split  46414  sge0seq  46451  caragensspw  46514  omessre  46515  caragendifcl  46519  caratheodorylem1  46531  0ome  46534  omess0  46539  caragencmpl  46540  hoicvr  46553  hoissrrn  46554  hoicvrrex  46561  ovnlecvr  46563  ovnsslelem  46565  ovnssle  46566  ovnsubaddlem1  46575  hoissrrn2  46583  hoidmv1lelem1  46596  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem4  46603  ovnlecvr2  46615  voncmpl  46626  hspmbl  46634  opnvonmbllem1  46637  ovolval5lem2  46658  ovolval5lem3  46659  vonioolem1  46685  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  issmflem  46732  cnfsmf  46745  incsmflem  46746  smfsssmf  46748  smfadd  46770  decsmflem  46771  smflim  46782  smfres  46795  smfmul  46800  smfpimbor1lem1  46803  smfco  46807  smfsuplem1  46816  smfsuplem3  46818  smflimsuplem1  46825  smflimsuplem4  46828  smflimsuplem7  46831  cnneiima  48909  seposep  48918  iscnrm3rlem4  48935  iscnrm3llem1  48941  lubsscl  48952  glbsscl  48953  toplatglb  48993  setrecsss  49694  elpglem1  49704