Theorem sstrd 3957

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

Syntax hints:   → wi 4   ⊆ wss 3914

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 3931

This theorem is referenced by:  sstrid  3958  sstrdi  3959  rabssrabd  4046  ssdif2d  4111  uniintsn  4949  funss  6535  fssxp  6715  knatar  7332  tfisi  7835  suppssov1  8176  suppssov2  8177  suppssfv  8181  tposss  8206  frrlem8  8272  tfrlem1  8344  omwordri  8536  oewordri  8556  oeeui  8566  oaabs2  8613  omopthlem1  8623  ecinxp  8765  sbthlem1  9051  dffi2  9374  hartogslem1  9495  cantnfcl  9620  cantnflt  9625  cantnfp1lem3  9633  cantnflem3  9644  cnfcom  9653  cnfcom3lem  9656  ttrcltr  9669  rankssb  9801  tskwe  9903  dfac12lem2  10098  dfac12lem3  10099  cfflb  10212  cfcof  10227  ssfin2  10273  hsmexlem4  10382  ttukeylem6  10467  ttukeylem7  10468  fpwwe2lem1  10584  fpwwe2lem7  10590  fpwwe2lem10  10593  fpwwe2lem11  10594  canthnumlem  10601  canthwelem  10603  canthwe  10604  canthp1lem2  10606  pwfseqlem5  10616  wunex2  10691  tsktrss  10714  inttsk  10727  uzwo3  12902  xrsupssd  13293  supicc  13462  supiccub  13463  supicclub  13464  ssfzunsnext  13530  seqsplit  14000  seqf1olem2a  14005  seqz  14015  swrdval2  14611  trrelssd  14939  rtrclreclem4  15027  sumss  15690  qshash  15793  incexc  15803  incexc2  15804  prodss  15913  rpnnen2lem11  16192  vdwlem1  16952  ramub1lem1  16997  imasaddvallem  17492  imasvscaf  17502  mrerintcl  17558  ismred2  17564  mremre  17565  mrcuni  17582  mressmrcd  17588  submrc  17589  mrissmrid  17602  mreexexlem2d  17606  isacs2  17614  isacs1i  17618  invss  17723  ssctr  17787  funcres2b  17859  isacs3lem  18501  acsfiindd  18512  acsmapd  18513  acsmap2d  18514  tsrdir  18563  subsubmgm  18637  subsubm  18743  gsumwspan  18773  subsubg  19081  subgint  19082  cntzidss  19272  symggen  19400  pmtrdifellem1  19406  pmtrdifellem2  19407  pgpssslw  19544  lsmless1x  19574  lsmless2x  19575  lsmless12  19592  subglsm  19603  gsumval3lem2  19836  gsumzaddlem  19851  gsumzadd  19852  gsum2d  19902  dmdprdd  19931  dprdfeq0  19954  dprdspan  19959  dprdres  19960  dprdss  19961  dprdz  19962  subgdmdprd  19966  subgdprd  19967  dprdsn  19968  dprd2dlem1  19973  dprd2da  19974  dmdprdsplit2lem  19977  dprdsplit  19980  pgpfac1lem2  20007  pgpfac1lem3  20009  pgpfac1lem5  20011  subsubrng  20472  subsubrg  20507  subdrgint  20712  lspss  20890  lspun  20893  lsslsp  20921  lsslspOLD  20922  lmhmlsp  20956  lsmelval2  20992  lsmssspx  20995  lsppratlem2  21058  lsppratlem3  21059  lsppratlem4  21060  lbsextlem2  21069  lbsextlem3  21070  ocvlsp  21585  cssmre  21602  obselocv  21637  obslbs  21639  aspss  21786  mhpaddcl  22038  mhpinvcl  22039  mhpvscacl  22041  psdmullem  22052  toponmre  22980  neiint  22991  neiss  22996  lpss  23029  lpss3  23031  restopnb  23062  restfpw  23066  neitr  23067  restcls  23068  restntr  23069  restlp  23070  ordtbas  23079  pnfnei  23107  mnfnei  23108  iscnp4  23150  cnclsi  23159  isreg2  23264  discmp  23285  cmpcld  23289  uncmp  23290  sscmp  23292  hauscmplem  23293  cmpfi  23295  iunconnlem  23314  clsconn  23317  2ndcctbss  23342  restnlly  23369  llyrest  23372  nllyrest  23373  llyidm  23375  nllyidm  23376  cldllycmp  23382  dislly  23384  comppfsc  23419  llycmpkgen2  23437  ptbasfi  23468  txnlly  23524  txcmplem1  23528  tx1stc  23537  xkococnlem  23546  qtopval2  23583  basqtop  23598  tgqtop  23599  qtoprest  23604  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  fsubbas  23754  fgabs  23766  fbasrn  23771  trfil2  23774  trfg  23778  isufil2  23795  trufil  23797  ssufl  23805  ufileu  23806  filufint  23807  fmfnfmlem4  23844  fmfnfm  23845  flimss2  23859  flimss1  23860  fclsfnflim  23914  flimfnfcls  23915  fclscmp  23917  cnpfcfi  23927  alexsubALT  23938  clssubg  23996  clsnsg  23997  tsmsres  24031  ustexsym  24103  ustex2sym  24104  ustex3sym  24105  ustneism  24111  trust  24117  utoptop  24122  restutopopn  24126  utop2nei  24138  utopreg  24140  cfiluweak  24182  neipcfilu  24183  blssps  24312  blss  24313  blcld  24393  blsscls  24395  met1stc  24409  met2ndci  24410  metust  24446  cfilucfil  24447  restmetu  24458  tgqioo  24688  xrsblre  24700  reconnlem2  24716  xrge0gsumle  24722  xrge0tsms  24723  rescncf  24790  cnmpopc  24822  cnheibor  24854  cnllycmp  24855  lebnum  24863  phtpycn  24882  cfilfcls  25174  iscmet3lem2  25192  cmetss  25216  cncmet  25222  bcthlem4  25227  bcth3  25231  rrxcph  25292  rrxmetlem  25307  minveclem4a  25330  minveclem4  25332  ivthicc  25359  ovollb  25380  ovollb2lem  25389  ovollb2  25390  nulmbl2  25437  ioorcl2  25473  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  opnmbllem  25502  volcn  25507  volivth  25508  mbfeqalem1  25542  itg10a  25611  mbfi1fseqlem4  25619  ditgcl  25759  ditgswap  25760  ditgsplitlem  25761  limcflf  25782  limcres  25787  dvbss  25802  dvbsss  25803  perfdvf  25804  dvreslem  25810  dvres2lem  25811  dvres3  25814  dvmptresicc  25817  dvcnp  25820  dvcnp2  25821  dvcnp2OLD  25822  dvcn  25823  dvnff  25825  dvn2bss  25832  dvnres  25833  cpnord  25837  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvnfre  25856  dvmptres2  25866  dvmptntr  25875  dvcnvlem  25880  dvcnv  25881  dvferm1lem  25888  dvferm2lem  25890  dvlip  25898  dvlipcn  25899  dvlip2  25900  c1liplem1  25901  dvgt0lem1  25907  lhop1lem  25918  lhop  25921  dvcnvrelem1  25922  dvcnvrelem2  25923  dvcnvre  25924  dvfsumle  25926  dvfsumleOLD  25927  dvfsumge  25928  dvfsumabs  25929  ftc1lem1  25942  ftc1lem2  25943  ftc1a  25944  ftc1lem4  25946  ftc2ditglem  25952  itgsubstlem  25955  ig1peu  26080  ig1pdvds  26085  taylfvallem1  26264  tayl0  26269  taylply2  26275  taylply2OLD  26276  taylply  26277  dvtaylp  26278  dvntaylp  26279  dvntaylp0  26280  taylthlem1  26281  ulmdvlem1  26309  ulmdvlem3  26311  psercn  26336  pserdvlem2  26338  abelth  26351  xrlimcnp  26878  lgamucov  26948  wilthlem2  26979  sqff1o  27092  chtublem  27122  pntlemq  27512  pntlemf  27516  sssslt1  27707  sssslt2  27708  scutbdaybnd  27727  scutbdaybnd2  27728  cofss  27838  coiniss  27839  tglineintmo  28569  ttgcontlem1  28812  pthdlem1  29696  shintcli  31258  shub1  31311  mdslmd1lem1  32254  mdexchi  32264  chirredlem1  32319  mdsymlem5  32336  sumdmdii  32344  sumdmdlem2  32348  fnpreimac  32595  fsuppinisegfi  32610  xrge0infssd  32684  swrdrn3  32877  swrdf1  32878  swrdrndisj  32879  pwrssmgc  32926  xrge0tsmsd  33002  elrgspnlem4  33196  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  fldgenss  33266  fldgenssp  33268  linds2eq  33352  elrspunidl  33399  ssdifidllem  33427  ssdifidlprm  33429  mxidlprm  33441  ssmxidllem  33444  ssmxidl  33445  qsdrnglem2  33467  rprmdvdsprod  33505  ressply1evls1  33534  resssra  33583  lsssra  33584  exsslsb  33592  lbsdiflsp0  33622  dimkerim  33623  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  dimlssid  33628  fldextrspunlsplem  33668  fldextrspunlsp  33669  fldextrspunlem1  33670  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  constr01  33732  constrmon  33734  constrextdg2lem  33738  constrfiss  33741  smatrcl  33786  locfinreflem  33830  cmpcref  33840  zarclsun  33860  zarclsiin  33861  zarclssn  33863  zarcmplem  33871  pnfneige0  33941  esum2d  34083  insiga  34127  sssigagen2  34136  dynkin  34157  dya2iocnei  34273  omsmon  34289  carsgclctunlem1  34308  carsggect  34309  omsmeas  34314  ftc2re  34589  fdvneggt  34591  fdvnegge  34593  reprsuc  34606  reprss  34608  reprlt  34610  reprinfz1  34613  logdivsqrle  34641  hgt750lemb  34647  bnj906  34920  bnj1020  34955  bnj1137  34985  bnj1408  35026  bnj1452  35042  erdszelem7  35184  erdszelem8  35185  erdsze2lem1  35190  connpconn  35222  cvmliftmolem1  35268  cvmlift2lem1  35289  cvmlift2lem9  35298  cvmlift2lem10  35299  cvmlift3lem6  35311  cvmlift3lem7  35312  satfsschain  35351  ss2mcls  35555  neibastop2lem  36348  fnemeet2  36355  fnejoin1  36356  ontgval  36419  unbdqndv1  36496  opnmbllem0  37650  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  sstotbnd2  37768  heiborlem1  37805  heiborlem8  37812  intidl  38023  lsmsat  39001  lssats  39005  lpssat  39006  lssatle  39008  lssat  39009  lsatcvatlem  39042  paddss12  39813  paddasslem17  39830  pmodlem1  39840  pmod1i  39842  pmodl42N  39845  elpcliN  39887  pclfinN  39894  polcon3N  39911  polcon2N  39913  paddunN  39921  pclfinclN  39944  poml5N  39948  osumcllem1N  39950  osumcllem2N  39951  osumcllem3N  39952  pl42lem2N  39974  pl42lem4N  39976  cdlemn5pre  41194  dihord1  41212  dihord2a  41213  dihord2b  41214  dihord5b  41253  dochss  41359  dochdmj1  41384  djhsumss  41401  djhunssN  41403  dochexmidlem2  41455  lclkrslem1  41531  lclkrslem2  41532  lcfrlem2  41537  aks4d1p4  42067  aks4d1p5  42068  aks4d1p7  42071  aks4d1p8  42075  aks6d1c2  42118  sticksstones1  42134  unitscyglem5  42187  prjcrv0  42621  elrfi  42682  ismrcd1  42686  istopclsd  42688  mrefg2  42695  aomclem2  43044  aomclem6  43048  hbtlem6  43118  hbt  43119  oege2  43296  cantnftermord  43309  omabs2  43321  tfsconcat0b  43335  naddgeoa  43383  naddwordnexlem0  43385  naddwordnexlem1  43386  dfno2  43417  mptrcllem  43602  dfrcl2  43663  relexp0a  43705  trclimalb2  43715  frege81d  43736  k0004ss2  44141  imo72b2lem2  44156  imo72b2  44161  uzwo4  45047  ssin0  45049  ixpssmapc  45067  ssinc  45081  ssdec  45082  supxrre3  45321  uzfissfz  45322  ssuzfz  45345  supminfxr  45460  inficc  45532  ressiocsup  45552  ressioosup  45553  ressiooinf  45555  limccog  45618  limclner  45649  limsupres  45703  limsupresuz2  45707  limsupequzlem  45720  supcnvlimsup  45738  limsupgtlem  45775  liminfresuz2  45785  cncfmptssg  45869  cncfuni  45884  icccncfext  45885  dvresntr  45916  dvbdfbdioolem1  45926  dvdmsscn  45934  dvnxpaek  45940  dvnprodlem2  45945  stoweidlem59  46057  fourierdlem20  46125  fourierdlem42  46147  fourierdlem48  46152  fourierdlem49  46153  fourierdlem52  46156  fourierdlem58  46162  fourierdlem64  46168  fourierdlem73  46177  fourierdlem76  46180  fourierdlem80  46184  fourierdlem84  46188  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  fourierdlem113  46217  etransclem18  46250  ioorrnopnlem  46302  salincl  46322  intsal  46328  fsumlesge0  46375  sge0cl  46379  sge0supre  46387  sge0less  46390  sge0split  46407  sge0seq  46444  caragensspw  46507  omessre  46508  caragendifcl  46512  caratheodorylem1  46524  0ome  46527  omess0  46532  caragencmpl  46533  hoicvr  46546  hoissrrn  46547  hoicvrrex  46554  ovnlecvr  46556  ovnsslelem  46558  ovnssle  46559  ovnsubaddlem1  46568  hoissrrn2  46576  hoidmv1lelem1  46589  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem4  46596  ovnlecvr2  46608  voncmpl  46619  hspmbl  46627  opnvonmbllem1  46630  ovolval5lem2  46651  ovolval5lem3  46652  vonioolem1  46678  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  issmflem  46725  cnfsmf  46738  incsmflem  46739  smfsssmf  46741  smfadd  46763  decsmflem  46764  smflim  46775  smfres  46788  smfmul  46793  smfpimbor1lem1  46796  smfco  46800  smfsuplem1  46809  smfsuplem3  46811  smflimsuplem1  46818  smflimsuplem4  46821  smflimsuplem7  46824  cnneiima  48905  seposep  48914  iscnrm3rlem4  48931  iscnrm3llem1  48937  lubsscl  48948  glbsscl  48949  toplatglb  48989  setrecsss  49690  elpglem1  49700