Theorem sstrd 3948

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

Syntax hints:   → wi 4   ⊆ wss 3905

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 3922

This theorem is referenced by:  sstrid  3949  sstrdi  3950  rabssrabd  4036  ssdif2d  4101  uniintsn  4938  funss  6505  fssxp  6683  knatar  7298  tfisi  7799  suppssov1  8137  suppssov2  8138  suppssfv  8142  tposss  8167  frrlem8  8233  tfrlem1  8305  omwordri  8497  oewordri  8517  oeeui  8527  oaabs2  8574  omopthlem1  8584  ecinxp  8726  sbthlem1  9011  dffi2  9332  hartogslem1  9453  cantnfcl  9582  cantnflt  9587  cantnfp1lem3  9595  cantnflem3  9606  cnfcom  9615  cnfcom3lem  9618  ttrcltr  9631  rankssb  9763  tskwe  9865  dfac12lem2  10058  dfac12lem3  10059  cfflb  10172  cfcof  10187  ssfin2  10233  hsmexlem4  10342  ttukeylem6  10427  ttukeylem7  10428  fpwwe2lem1  10544  fpwwe2lem7  10550  fpwwe2lem10  10553  fpwwe2lem11  10554  canthnumlem  10561  canthwelem  10563  canthwe  10564  canthp1lem2  10566  pwfseqlem5  10576  wunex2  10651  tsktrss  10674  inttsk  10687  uzwo3  12862  xrsupssd  13253  supicc  13422  supiccub  13423  supicclub  13424  ssfzunsnext  13490  seqsplit  13960  seqf1olem2a  13965  seqz  13975  swrdval2  14571  trrelssd  14898  rtrclreclem4  14986  sumss  15649  qshash  15752  incexc  15762  incexc2  15763  prodss  15872  rpnnen2lem11  16151  vdwlem1  16911  ramub1lem1  16956  imasaddvallem  17451  imasvscaf  17461  mrerintcl  17517  ismred2  17523  mremre  17524  mrcuni  17545  mressmrcd  17551  submrc  17552  mrissmrid  17565  mreexexlem2d  17569  isacs2  17577  isacs1i  17581  invss  17686  ssctr  17750  funcres2b  17822  isacs3lem  18466  acsfiindd  18477  acsmapd  18478  acsmap2d  18479  tsrdir  18528  subsubmgm  18602  subsubm  18708  gsumwspan  18738  subsubg  19046  subgint  19047  cntzidss  19237  symggen  19367  pmtrdifellem1  19373  pmtrdifellem2  19374  pgpssslw  19511  lsmless1x  19541  lsmless2x  19542  lsmless12  19559  subglsm  19570  gsumval3lem2  19803  gsumzaddlem  19818  gsumzadd  19819  gsum2d  19869  dmdprdd  19898  dprdfeq0  19921  dprdspan  19926  dprdres  19927  dprdss  19928  dprdz  19929  subgdmdprd  19933  subgdprd  19934  dprdsn  19935  dprd2dlem1  19940  dprd2da  19941  dmdprdsplit2lem  19944  dprdsplit  19947  pgpfac1lem2  19974  pgpfac1lem3  19976  pgpfac1lem5  19978  subsubrng  20466  subsubrg  20501  subdrgint  20706  lspss  20905  lspun  20908  lsslsp  20936  lsslspOLD  20937  lmhmlsp  20971  lsmelval2  21007  lsmssspx  21010  lsppratlem2  21073  lsppratlem3  21074  lsppratlem4  21075  lbsextlem2  21084  lbsextlem3  21085  ocvlsp  21601  cssmre  21618  obselocv  21653  obslbs  21655  aspss  21802  mhpaddcl  22054  mhpinvcl  22055  mhpvscacl  22057  psdmullem  22068  toponmre  22996  neiint  23007  neiss  23012  lpss  23045  lpss3  23047  restopnb  23078  restfpw  23082  neitr  23083  restcls  23084  restntr  23085  restlp  23086  ordtbas  23095  pnfnei  23123  mnfnei  23124  iscnp4  23166  cnclsi  23175  isreg2  23280  discmp  23301  cmpcld  23305  uncmp  23306  sscmp  23308  hauscmplem  23309  cmpfi  23311  iunconnlem  23330  clsconn  23333  2ndcctbss  23358  restnlly  23385  llyrest  23388  nllyrest  23389  llyidm  23391  nllyidm  23392  cldllycmp  23398  dislly  23400  comppfsc  23435  llycmpkgen2  23453  ptbasfi  23484  txnlly  23540  txcmplem1  23544  tx1stc  23553  xkococnlem  23562  qtopval2  23599  basqtop  23614  tgqtop  23615  qtoprest  23620  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  fsubbas  23770  fgabs  23782  fbasrn  23787  trfil2  23790  trfg  23794  isufil2  23811  trufil  23813  ssufl  23821  ufileu  23822  filufint  23823  fmfnfmlem4  23860  fmfnfm  23861  flimss2  23875  flimss1  23876  fclsfnflim  23930  flimfnfcls  23931  fclscmp  23933  cnpfcfi  23943  alexsubALT  23954  clssubg  24012  clsnsg  24013  tsmsres  24047  ustexsym  24119  ustex2sym  24120  ustex3sym  24121  ustneism  24127  trust  24133  utoptop  24138  restutopopn  24142  utop2nei  24154  utopreg  24156  cfiluweak  24198  neipcfilu  24199  blssps  24328  blss  24329  blcld  24409  blsscls  24411  met1stc  24425  met2ndci  24426  metust  24462  cfilucfil  24463  restmetu  24474  tgqioo  24704  xrsblre  24716  reconnlem2  24732  xrge0gsumle  24738  xrge0tsms  24739  rescncf  24806  cnmpopc  24838  cnheibor  24870  cnllycmp  24871  lebnum  24879  phtpycn  24898  cfilfcls  25190  iscmet3lem2  25208  cmetss  25232  cncmet  25238  bcthlem4  25243  bcth3  25247  rrxcph  25308  rrxmetlem  25323  minveclem4a  25346  minveclem4  25348  ivthicc  25375  ovollb  25396  ovollb2lem  25405  ovollb2  25406  nulmbl2  25453  ioorcl2  25489  uniioombllem3  25502  uniioombllem4  25503  uniioombllem5  25504  opnmbllem  25518  volcn  25523  volivth  25524  mbfeqalem1  25558  itg10a  25627  mbfi1fseqlem4  25635  ditgcl  25775  ditgswap  25776  ditgsplitlem  25777  limcflf  25798  limcres  25803  dvbss  25818  dvbsss  25819  perfdvf  25820  dvreslem  25826  dvres2lem  25827  dvres3  25830  dvmptresicc  25833  dvcnp  25836  dvcnp2  25837  dvcnp2OLD  25838  dvcn  25839  dvnff  25841  dvn2bss  25848  dvnres  25849  cpnord  25853  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcobr  25865  dvcobrOLD  25866  dvnfre  25872  dvmptres2  25882  dvmptntr  25891  dvcnvlem  25896  dvcnv  25897  dvferm1lem  25904  dvferm2lem  25906  dvlip  25914  dvlipcn  25915  dvlip2  25916  c1liplem1  25917  dvgt0lem1  25923  lhop1lem  25934  lhop  25937  dvcnvrelem1  25938  dvcnvrelem2  25939  dvcnvre  25940  dvfsumle  25942  dvfsumleOLD  25943  dvfsumge  25944  dvfsumabs  25945  ftc1lem1  25958  ftc1lem2  25959  ftc1a  25960  ftc1lem4  25962  ftc2ditglem  25968  itgsubstlem  25971  ig1peu  26096  ig1pdvds  26101  taylfvallem1  26280  tayl0  26285  taylply2  26291  taylply2OLD  26292  taylply  26293  dvtaylp  26294  dvntaylp  26295  dvntaylp0  26296  taylthlem1  26297  ulmdvlem1  26325  ulmdvlem3  26327  psercn  26352  pserdvlem2  26354  abelth  26367  xrlimcnp  26894  lgamucov  26964  wilthlem2  26995  sqff1o  27108  chtublem  27138  pntlemq  27528  pntlemf  27532  sssslt1  27724  sssslt2  27725  scutbdaybnd  27744  scutbdaybnd2  27745  eqscut3  27753  cofss  27861  coiniss  27862  tglineintmo  28605  ttgcontlem1  28848  pthdlem1  29729  shintcli  31291  shub1  31344  mdslmd1lem1  32287  mdexchi  32297  chirredlem1  32352  mdsymlem5  32369  sumdmdii  32377  sumdmdlem2  32381  fnpreimac  32628  fsuppinisegfi  32643  xrge0infssd  32717  swrdrn3  32910  swrdf1  32911  swrdrndisj  32912  pwrssmgc  32955  xrge0tsmsd  33028  elrgspnlem4  33198  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  fldgenss  33268  fldgenssp  33270  linds2eq  33331  elrspunidl  33378  ssdifidllem  33406  ssdifidlprm  33408  mxidlprm  33420  ssmxidllem  33423  ssmxidl  33424  qsdrnglem2  33446  rprmdvdsprod  33484  ressply1evls1  33513  resssra  33562  lsssra  33563  exsslsb  33571  lbsdiflsp0  33601  dimkerim  33602  fedgmullem1  33604  fedgmullem2  33605  fedgmul  33606  dimlssid  33607  fldextrspunlsplem  33647  fldextrspunlsp  33648  fldextrspunlem1  33649  fldextrspundgdvdslem  33654  fldextrspundgdvds  33655  constr01  33711  constrmon  33713  constrextdg2lem  33717  constrfiss  33720  smatrcl  33765  locfinreflem  33809  cmpcref  33819  zarclsun  33839  zarclsiin  33840  zarclssn  33842  zarcmplem  33850  pnfneige0  33920  esum2d  34062  insiga  34106  sssigagen2  34115  dynkin  34136  dya2iocnei  34252  omsmon  34268  carsgclctunlem1  34287  carsggect  34288  omsmeas  34293  ftc2re  34568  fdvneggt  34570  fdvnegge  34572  reprsuc  34585  reprss  34587  reprlt  34589  reprinfz1  34592  logdivsqrle  34620  hgt750lemb  34626  bnj906  34899  bnj1020  34934  bnj1137  34964  bnj1408  35005  bnj1452  35021  erdszelem7  35172  erdszelem8  35173  erdsze2lem1  35178  connpconn  35210  cvmliftmolem1  35256  cvmlift2lem1  35277  cvmlift2lem9  35286  cvmlift2lem10  35287  cvmlift3lem6  35299  cvmlift3lem7  35300  satfsschain  35339  ss2mcls  35543  neibastop2lem  36336  fnemeet2  36343  fnejoin1  36344  ontgval  36407  unbdqndv1  36484  opnmbllem0  37638  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  sstotbnd2  37756  heiborlem1  37793  heiborlem8  37800  intidl  38011  lsmsat  38989  lssats  38993  lpssat  38994  lssatle  38996  lssat  38997  lsatcvatlem  39030  paddss12  39801  paddasslem17  39818  pmodlem1  39828  pmod1i  39830  pmodl42N  39833  elpcliN  39875  pclfinN  39882  polcon3N  39899  polcon2N  39901  paddunN  39909  pclfinclN  39932  poml5N  39936  osumcllem1N  39938  osumcllem2N  39939  osumcllem3N  39940  pl42lem2N  39962  pl42lem4N  39964  cdlemn5pre  41182  dihord1  41200  dihord2a  41201  dihord2b  41202  dihord5b  41241  dochss  41347  dochdmj1  41372  djhsumss  41389  djhunssN  41391  dochexmidlem2  41443  lclkrslem1  41519  lclkrslem2  41520  lcfrlem2  41525  aks4d1p4  42055  aks4d1p5  42056  aks4d1p7  42059  aks4d1p8  42063  aks6d1c2  42106  sticksstones1  42122  unitscyglem5  42175  prjcrv0  42609  elrfi  42670  ismrcd1  42674  istopclsd  42676  mrefg2  42683  aomclem2  43031  aomclem6  43035  hbtlem6  43105  hbt  43106  oege2  43283  cantnftermord  43296  omabs2  43308  tfsconcat0b  43322  naddgeoa  43370  naddwordnexlem0  43372  naddwordnexlem1  43373  dfno2  43404  mptrcllem  43589  dfrcl2  43650  relexp0a  43692  trclimalb2  43702  frege81d  43723  k0004ss2  44128  imo72b2lem2  44143  imo72b2  44148  uzwo4  45034  ssin0  45036  ixpssmapc  45054  ssinc  45068  ssdec  45069  supxrre3  45308  uzfissfz  45309  ssuzfz  45332  supminfxr  45447  inficc  45519  ressiocsup  45539  ressioosup  45540  ressiooinf  45542  limccog  45605  limclner  45636  limsupres  45690  limsupresuz2  45694  limsupequzlem  45707  supcnvlimsup  45725  limsupgtlem  45762  liminfresuz2  45772  cncfmptssg  45856  cncfuni  45871  icccncfext  45872  dvresntr  45903  dvbdfbdioolem1  45913  dvdmsscn  45921  dvnxpaek  45927  dvnprodlem2  45932  stoweidlem59  46044  fourierdlem20  46112  fourierdlem42  46134  fourierdlem48  46139  fourierdlem49  46140  fourierdlem52  46143  fourierdlem58  46149  fourierdlem64  46155  fourierdlem73  46164  fourierdlem76  46167  fourierdlem80  46171  fourierdlem84  46175  fourierdlem93  46184  fourierdlem103  46194  fourierdlem104  46195  fourierdlem113  46204  etransclem18  46237  ioorrnopnlem  46289  salincl  46309  intsal  46315  fsumlesge0  46362  sge0cl  46366  sge0supre  46374  sge0less  46377  sge0split  46394  sge0seq  46431  caragensspw  46494  omessre  46495  caragendifcl  46499  caratheodorylem1  46511  0ome  46514  omess0  46519  caragencmpl  46520  hoicvr  46533  hoissrrn  46534  hoicvrrex  46541  ovnlecvr  46543  ovnsslelem  46545  ovnssle  46546  ovnsubaddlem1  46555  hoissrrn2  46563  hoidmv1lelem1  46576  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem4  46583  ovnlecvr2  46595  voncmpl  46606  hspmbl  46614  opnvonmbllem1  46617  ovolval5lem2  46638  ovolval5lem3  46639  vonioolem1  46665  pimdecfgtioc  46700  pimincfltioc  46701  pimdecfgtioo  46702  pimincfltioo  46703  issmflem  46712  cnfsmf  46725  incsmflem  46726  smfsssmf  46728  smfadd  46750  decsmflem  46751  smflim  46762  smfres  46775  smfmul  46780  smfpimbor1lem1  46783  smfco  46787  smfsuplem1  46796  smfsuplem3  46798  smflimsuplem1  46805  smflimsuplem4  46808  smflimsuplem7  46811  cnneiima  48905  seposep  48914  iscnrm3rlem4  48931  iscnrm3llem1  48937  lubsscl  48948  glbsscl  48949  toplatglb  48989  setrecsss  49690  elpglem1  49700