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

Syntax hints:   → wi 4   ⊆ wss 3890

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ss 3907

This theorem is referenced by:  sstrid  3933  sstrdi  3934  rabssrabd  4021  ssdif2d  4085  uniintsn  4922  funss  6511  fssxp  6689  knatar  7308  tfisi  7806  suppssov1  8144  suppssov2  8145  suppssfv  8149  tposss  8174  frrlem8  8240  tfrlem1  8312  omwordri  8504  oewordri  8525  oeeui  8535  oaabs2  8582  omopthlem1  8592  ecinxp  8736  sbthlem1  9022  dffi2  9333  hartogslem1  9454  cantnfcl  9586  cantnflt  9591  cantnfp1lem3  9599  cantnflem3  9610  cnfcom  9619  cnfcom3lem  9622  ttrcltr  9635  rankssb  9770  tskwe  9872  dfac12lem2  10065  dfac12lem3  10066  cfflb  10179  cfcof  10194  ssfin2  10240  hsmexlem4  10349  ttukeylem6  10434  ttukeylem7  10435  fpwwe2lem1  10552  fpwwe2lem7  10558  fpwwe2lem10  10561  fpwwe2lem11  10562  canthnumlem  10569  canthwelem  10571  canthwe  10572  canthp1lem2  10574  pwfseqlem5  10584  wunex2  10659  tsktrss  10682  inttsk  10695  uzwo3  12891  xrsupssd  13283  supicc  13452  supiccub  13453  supicclub  13454  ssfzunsnext  13521  seqsplit  13995  seqf1olem2a  14000  seqz  14010  swrdval2  14607  trrelssd  14933  rtrclreclem4  15021  sumss  15684  qshash  15788  incexc  15800  incexc2  15801  prodss  15910  rpnnen2lem11  16189  vdwlem1  16950  ramub1lem1  16995  imasaddvallem  17491  imasvscaf  17501  mrerintcl  17557  ismred2  17563  mremre  17564  mrcuni  17585  mressmrcd  17591  submrc  17592  mrissmrid  17605  mreexexlem2d  17609  isacs2  17617  isacs1i  17621  invss  17726  ssctr  17790  funcres2b  17862  isacs3lem  18506  acsfiindd  18517  acsmapd  18518  acsmap2d  18519  tsrdir  18568  subsubmgm  18676  subsubm  18782  gsumwspan  18812  subsubg  19123  subgint  19124  cntzidss  19313  symggen  19443  pmtrdifellem1  19449  pmtrdifellem2  19450  pgpssslw  19587  lsmless1x  19617  lsmless2x  19618  lsmless12  19635  subglsm  19646  gsumval3lem2  19879  gsumzaddlem  19894  gsumzadd  19895  gsum2d  19945  dmdprdd  19974  dprdfeq0  19997  dprdspan  20002  dprdres  20003  dprdss  20004  dprdz  20005  subgdmdprd  20009  subgdprd  20010  dprdsn  20011  dprd2dlem1  20016  dprd2da  20017  dmdprdsplit2lem  20020  dprdsplit  20023  pgpfac1lem2  20050  pgpfac1lem3  20052  pgpfac1lem5  20054  subsubrng  20542  subsubrg  20577  subdrgint  20782  lspss  20981  lspun  20984  lsslsp  21012  lmhmlsp  21046  lsmelval2  21082  lsmssspx  21085  lsppratlem2  21148  lsppratlem3  21149  lsppratlem4  21150  lbsextlem2  21159  lbsextlem3  21160  ocvlsp  21658  cssmre  21675  obselocv  21710  obslbs  21712  aspss  21858  mhpaddcl  22146  mhpinvcl  22147  mhpvscacl  22149  psdmullem  22160  toponmre  23083  neiint  23094  neiss  23099  lpss  23132  lpss3  23134  restopnb  23165  restfpw  23169  neitr  23170  restcls  23171  restntr  23172  restlp  23173  ordtbas  23182  pnfnei  23210  mnfnei  23211  iscnp4  23253  cnclsi  23262  isreg2  23367  discmp  23388  cmpcld  23392  uncmp  23393  sscmp  23395  hauscmplem  23396  cmpfi  23398  iunconnlem  23417  clsconn  23420  2ndcctbss  23445  restnlly  23472  llyrest  23475  nllyrest  23476  llyidm  23478  nllyidm  23479  cldllycmp  23485  dislly  23487  comppfsc  23522  llycmpkgen2  23540  ptbasfi  23571  txnlly  23627  txcmplem1  23631  tx1stc  23640  xkococnlem  23649  qtopval2  23686  basqtop  23701  tgqtop  23702  qtoprest  23707  kqreglem1  23731  kqreglem2  23732  kqnrmlem1  23733  kqnrmlem2  23734  fsubbas  23857  fgabs  23869  fbasrn  23874  trfil2  23877  trfg  23881  isufil2  23898  trufil  23900  ssufl  23908  ufileu  23909  filufint  23910  fmfnfmlem4  23947  fmfnfm  23948  flimss2  23962  flimss1  23963  fclsfnflim  24017  flimfnfcls  24018  fclscmp  24020  cnpfcfi  24030  alexsubALT  24041  clssubg  24099  clsnsg  24100  tsmsres  24134  ustexsym  24206  ustex2sym  24207  ustex3sym  24208  ustneism  24214  trust  24219  utoptop  24224  restutopopn  24228  utop2nei  24240  utopreg  24242  cfiluweak  24284  neipcfilu  24285  blssps  24414  blss  24415  blcld  24495  blsscls  24497  met1stc  24511  met2ndci  24512  metust  24548  cfilucfil  24549  restmetu  24560  tgqioo  24790  xrsblre  24802  reconnlem2  24818  xrge0gsumle  24824  xrge0tsms  24825  rescncf  24889  cnmpopc  24920  cnheibor  24947  cnllycmp  24948  lebnum  24956  phtpycn  24975  cfilfcls  25266  iscmet3lem2  25284  cmetss  25308  cncmet  25314  bcthlem4  25319  bcth3  25323  rrxcph  25384  rrxmetlem  25399  minveclem4a  25422  minveclem4  25424  ivthicc  25450  ovollb  25471  ovollb2lem  25480  ovollb2  25481  nulmbl2  25528  ioorcl2  25564  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  opnmbllem  25593  volcn  25598  volivth  25599  mbfeqalem1  25633  itg10a  25702  mbfi1fseqlem4  25710  ditgcl  25850  ditgswap  25851  ditgsplitlem  25852  limcflf  25873  limcres  25878  dvbss  25893  dvbsss  25894  perfdvf  25895  dvreslem  25901  dvres2lem  25902  dvres3  25905  dvmptresicc  25908  dvcnp  25911  dvcnp2  25912  dvcn  25913  dvnff  25915  dvn2bss  25922  dvnres  25923  cpnord  25927  dvaddbr  25930  dvmulbr  25931  dvcobr  25938  dvnfre  25944  dvmptres2  25954  dvmptntr  25963  dvcnvlem  25968  dvcnv  25969  dvferm1lem  25976  dvferm2lem  25978  dvlip  25985  dvlipcn  25986  dvlip2  25987  c1liplem1  25988  dvgt0lem1  25994  lhop1lem  26005  lhop  26008  dvcnvrelem1  26009  dvcnvrelem2  26010  dvcnvre  26011  dvfsumle  26013  dvfsumge  26014  dvfsumabs  26015  ftc1lem1  26027  ftc1lem2  26028  ftc1a  26029  ftc1lem4  26031  ftc2ditglem  26037  itgsubstlem  26040  ig1peu  26165  ig1pdvds  26170  taylfvallem1  26347  tayl0  26352  taylply2  26358  taylply  26359  dvtaylp  26360  dvntaylp  26361  dvntaylp0  26362  taylthlem1  26363  ulmdvlem1  26390  ulmdvlem3  26392  psercn  26416  pserdvlem2  26418  abelth  26431  xrlimcnp  26957  lgamucov  27026  wilthlem2  27057  sqff1o  27170  chtublem  27199  pntlemq  27589  pntlemf  27593  ssslts1  27790  ssslts2  27791  cutbdaybnd  27812  cutbdaybnd2  27813  eqcuts3  27821  cofss  27947  coiniss  27948  bdaypw2bnd  28482  bdayfinbndlem1  28484  z12bdaylem2  28488  tglineintmo  28735  ttgcontlem1  28978  pthdlem1  29859  shintcli  31425  shub1  31478  mdslmd1lem1  32421  mdexchi  32431  chirredlem1  32486  mdsymlem5  32503  sumdmdii  32511  sumdmdlem2  32515  fnpreimac  32769  fsuppinisegfi  32786  xrge0infssd  32860  swrdrn3  33041  swrdf1  33042  swrdrndisj  33043  pwrssmgc  33086  xrge0tsmsd  33161  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  fldgenss  33407  fldgenssp  33409  linds2eq  33471  elrspunidl  33518  ssdifidllem  33546  ssdifidlprm  33548  mxidlprm  33560  ssmxidllem  33563  ssmxidl  33564  qsdrnglem2  33586  rprmdvdsprod  33624  ressply1evls1  33655  resssra  33778  lsssra  33779  exsslsb  33788  lbsdiflsp0  33817  dimkerim  33818  fedgmullem1  33820  fedgmullem2  33821  fedgmul  33822  dimlssid  33823  fldextrspunlsplem  33864  fldextrspunlsp  33865  fldextrspunlem1  33866  fldextrspundgdvdslem  33871  fldextrspundgdvds  33872  constr01  33933  constrmon  33935  constrextdg2lem  33939  constrfiss  33942  smatrcl  33987  locfinreflem  34031  cmpcref  34041  zarclsun  34061  zarclsiin  34062  zarclssn  34064  zarcmplem  34072  pnfneige0  34142  esum2d  34284  insiga  34328  sssigagen2  34337  dynkin  34358  dya2iocnei  34473  omsmon  34489  carsgclctunlem1  34508  carsggect  34509  omsmeas  34514  ftc2re  34789  fdvneggt  34791  fdvnegge  34793  reprsuc  34806  reprss  34808  reprlt  34810  reprinfz1  34813  logdivsqrle  34841  hgt750lemb  34847  bnj906  35119  bnj1020  35154  bnj1137  35184  bnj1408  35225  bnj1452  35241  rankval4b  35288  fineqvnttrclselem2  35310  erdszelem7  35432  erdszelem8  35433  erdsze2lem1  35438  connpconn  35470  cvmliftmolem1  35516  cvmlift2lem1  35537  cvmlift2lem9  35546  cvmlift2lem10  35547  cvmlift3lem6  35559  cvmlift3lem7  35560  satfsschain  35599  ss2mcls  35803  neibastop2lem  36595  fnemeet2  36602  fnejoin1  36603  ontgval  36666  ttcmin  36731  unbdqndv1  36821  opnmbllem0  38030  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  sstotbnd2  38148  heiborlem1  38185  heiborlem8  38192  intidl  38403  lsmsat  39507  lssats  39511  lpssat  39512  lssatle  39514  lssat  39515  lsatcvatlem  39548  paddss12  40318  paddasslem17  40335  pmodlem1  40345  pmod1i  40347  pmodl42N  40350  elpcliN  40392  pclfinN  40399  polcon3N  40416  polcon2N  40418  paddunN  40426  pclfinclN  40449  poml5N  40453  osumcllem1N  40455  osumcllem2N  40456  osumcllem3N  40457  pl42lem2N  40479  pl42lem4N  40481  cdlemn5pre  41699  dihord1  41717  dihord2a  41718  dihord2b  41719  dihord5b  41758  dochss  41864  dochdmj1  41889  djhsumss  41906  djhunssN  41908  dochexmidlem2  41960  lclkrslem1  42036  lclkrslem2  42037  lcfrlem2  42042  aks4d1p4  42571  aks4d1p5  42572  aks4d1p7  42575  aks4d1p8  42579  aks6d1c2  42622  sticksstones1  42638  unitscyglem5  42691  prjcrv0  43090  elrfi  43150  ismrcd1  43154  istopclsd  43156  mrefg2  43163  aomclem2  43507  aomclem6  43511  hbtlem6  43581  hbt  43582  oege2  43759  cantnftermord  43772  omabs2  43784  tfsconcat0b  43798  naddgeoa  43846  naddwordnexlem0  43848  naddwordnexlem1  43849  dfno2  43879  mptrcllem  44064  dfrcl2  44125  relexp0a  44167  trclimalb2  44177  frege81d  44198  k0004ss2  44603  imo72b2lem2  44618  imo72b2  44623  uzwo4  45508  ssin0  45510  ixpssmapc  45528  ssinc  45541  ssdec  45542  supxrre3  45777  uzfissfz  45778  ssuzfz  45801  supminfxr  45914  inficc  45986  ressiocsup  46006  ressioosup  46007  ressiooinf  46009  limccog  46072  limclner  46101  limsupres  46155  limsupresuz2  46159  limsupequzlem  46172  supcnvlimsup  46190  limsupgtlem  46227  liminfresuz2  46237  cncfmptssg  46321  cncfuni  46336  icccncfext  46337  dvresntr  46368  dvbdfbdioolem1  46378  dvdmsscn  46386  dvnxpaek  46392  dvnprodlem2  46397  stoweidlem59  46509  fourierdlem20  46577  fourierdlem42  46599  fourierdlem48  46604  fourierdlem49  46605  fourierdlem52  46608  fourierdlem58  46614  fourierdlem64  46620  fourierdlem73  46629  fourierdlem76  46632  fourierdlem80  46636  fourierdlem84  46640  fourierdlem93  46649  fourierdlem103  46659  fourierdlem104  46660  fourierdlem113  46669  etransclem18  46702  ioorrnopnlem  46754  salincl  46774  intsal  46780  fsumlesge0  46827  sge0cl  46831  sge0supre  46839  sge0less  46842  sge0split  46859  sge0seq  46896  caragensspw  46959  omessre  46960  caragendifcl  46964  caratheodorylem1  46976  0ome  46979  omess0  46984  caragencmpl  46985  hoissrrn  46999  hoicvrrex  47006  ovnlecvr  47008  ovnsslelem  47010  ovnssle  47011  ovnsubaddlem1  47020  hoissrrn2  47028  hoidmv1lelem1  47041  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem4  47048  ovnlecvr2  47060  voncmpl  47071  hspmbl  47079  opnvonmbllem1  47082  ovolval5lem2  47103  ovolval5lem3  47104  vonioolem1  47130  pimdecfgtioc  47165  pimincfltioc  47166  pimdecfgtioo  47167  pimincfltioo  47168  issmflem  47177  cnfsmf  47190  incsmflem  47191  smfsssmf  47193  smfadd  47215  decsmflem  47216  smflim  47227  smfres  47240  smfmul  47245  smfpimbor1lem1  47248  smfco  47252  smfsuplem1  47261  smfsuplem3  47263  smflimsuplem1  47270  smflimsuplem4  47273  smflimsuplem7  47276  nndivides2  47854  cnneiima  49414  seposep  49423  iscnrm3rlem4  49440  iscnrm3llem1  49446  lubsscl  49457  glbsscl  49458  toplatglb  49498  setrecsss  50198  elpglem1  50208