Theorem sstrd 3994

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

Syntax hints:   → wi 4   ⊆ wss 3951

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 3968

This theorem is referenced by:  sstrid  3995  sstrdi  3996  rabssrabd  4083  ssdif2d  4148  uniintsn  4985  funss  6585  fssxp  6763  knatar  7377  tfisi  7880  suppssov1  8222  suppssov2  8223  suppssfv  8227  tposss  8252  frrlem8  8318  tfrlem1  8416  omwordri  8610  oewordri  8630  oeeui  8640  oaabs2  8687  omopthlem1  8697  ecinxp  8832  sbthlem1  9123  dffi2  9463  hartogslem1  9582  cantnfcl  9707  cantnflt  9712  cantnfp1lem3  9720  cantnflem3  9731  cnfcom  9740  cnfcom3lem  9743  ttrcltr  9756  rankssb  9888  tskwe  9990  dfac12lem2  10185  dfac12lem3  10186  cfflb  10299  cfcof  10314  ssfin2  10360  hsmexlem4  10469  ttukeylem6  10554  ttukeylem7  10555  fpwwe2lem1  10671  fpwwe2lem7  10677  fpwwe2lem10  10680  fpwwe2lem11  10681  canthnumlem  10688  canthwelem  10690  canthwe  10691  canthp1lem2  10693  pwfseqlem5  10703  wunex2  10778  tsktrss  10801  inttsk  10814  uzwo3  12985  supicc  13541  supiccub  13542  supicclub  13543  ssfzunsnext  13609  seqsplit  14076  seqf1olem2a  14081  seqz  14091  swrdval2  14684  trrelssd  15012  rtrclreclem4  15100  sumss  15760  qshash  15863  incexc  15873  incexc2  15874  prodss  15983  rpnnen2lem11  16260  vdwlem1  17019  ramub1lem1  17064  imasaddvallem  17574  imasvscaf  17584  mrerintcl  17640  ismred2  17646  mremre  17647  mrcuni  17664  mressmrcd  17670  submrc  17671  mrissmrid  17684  mreexexlem2d  17688  isacs2  17696  isacs1i  17700  invss  17805  ssctr  17869  funcres2b  17942  isacs3lem  18587  acsfiindd  18598  acsmapd  18599  acsmap2d  18600  tsrdir  18649  subsubmgm  18723  subsubm  18829  gsumwspan  18859  subsubg  19167  subgint  19168  cntzidss  19358  symggen  19488  pmtrdifellem1  19494  pmtrdifellem2  19495  pgpssslw  19632  lsmless1x  19662  lsmless2x  19663  lsmless12  19680  subglsm  19691  gsumval3lem2  19924  gsumzaddlem  19939  gsumzadd  19940  gsum2d  19990  dmdprdd  20019  dprdfeq0  20042  dprdspan  20047  dprdres  20048  dprdss  20049  dprdz  20050  subgdmdprd  20054  subgdprd  20055  dprdsn  20056  dprd2dlem1  20061  dprd2da  20062  dmdprdsplit2lem  20065  dprdsplit  20068  pgpfac1lem2  20095  pgpfac1lem3  20097  pgpfac1lem5  20099  subsubrng  20563  subsubrg  20598  subdrgint  20804  lspss  20982  lspun  20985  lsslsp  21013  lsslspOLD  21014  lmhmlsp  21048  lsmelval2  21084  lsmssspx  21087  lsppratlem2  21150  lsppratlem3  21151  lsppratlem4  21152  lbsextlem2  21161  lbsextlem3  21162  ocvlsp  21694  cssmre  21711  obselocv  21748  obslbs  21750  aspss  21897  mhpaddcl  22155  mhpinvcl  22156  mhpvscacl  22158  psdmullem  22169  toponmre  23101  neiint  23112  neiss  23117  lpss  23150  lpss3  23152  restopnb  23183  restfpw  23187  neitr  23188  restcls  23189  restntr  23190  restlp  23191  ordtbas  23200  pnfnei  23228  mnfnei  23229  iscnp4  23271  cnclsi  23280  isreg2  23385  discmp  23406  cmpcld  23410  uncmp  23411  sscmp  23413  hauscmplem  23414  cmpfi  23416  iunconnlem  23435  clsconn  23438  2ndcctbss  23463  restnlly  23490  llyrest  23493  nllyrest  23494  llyidm  23496  nllyidm  23497  cldllycmp  23503  dislly  23505  comppfsc  23540  llycmpkgen2  23558  ptbasfi  23589  txnlly  23645  txcmplem1  23649  tx1stc  23658  xkococnlem  23667  qtopval2  23704  basqtop  23719  tgqtop  23720  qtoprest  23725  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  fsubbas  23875  fgabs  23887  fbasrn  23892  trfil2  23895  trfg  23899  isufil2  23916  trufil  23918  ssufl  23926  ufileu  23927  filufint  23928  fmfnfmlem4  23965  fmfnfm  23966  flimss2  23980  flimss1  23981  fclsfnflim  24035  flimfnfcls  24036  fclscmp  24038  cnpfcfi  24048  alexsubALT  24059  clssubg  24117  clsnsg  24118  tsmsres  24152  ustexsym  24224  ustex2sym  24225  ustex3sym  24226  ustneism  24232  trust  24238  utoptop  24243  restutopopn  24247  utop2nei  24259  utopreg  24261  cfiluweak  24304  neipcfilu  24305  blssps  24434  blss  24435  blcld  24518  blsscls  24520  met1stc  24534  met2ndci  24535  metust  24571  cfilucfil  24572  restmetu  24583  tgqioo  24821  xrsblre  24833  reconnlem2  24849  xrge0gsumle  24855  xrge0tsms  24856  rescncf  24923  cnmpopc  24955  cnheibor  24987  cnllycmp  24988  lebnum  24996  phtpycn  25015  cfilfcls  25308  iscmet3lem2  25326  cmetss  25350  cncmet  25356  bcthlem4  25361  bcth3  25365  rrxcph  25426  rrxmetlem  25441  minveclem4a  25464  minveclem4  25466  ivthicc  25493  ovollb  25514  ovollb2lem  25523  ovollb2  25524  nulmbl2  25571  ioorcl2  25607  uniioombllem3  25620  uniioombllem4  25621  uniioombllem5  25622  opnmbllem  25636  volcn  25641  volivth  25642  mbfeqalem1  25676  itg10a  25745  mbfi1fseqlem4  25753  ditgcl  25893  ditgswap  25894  ditgsplitlem  25895  limcflf  25916  limcres  25921  dvbss  25936  dvbsss  25937  perfdvf  25938  dvreslem  25944  dvres2lem  25945  dvres3  25948  dvmptresicc  25951  dvcnp  25954  dvcnp2  25955  dvcnp2OLD  25956  dvcn  25957  dvnff  25959  dvn2bss  25966  dvnres  25967  cpnord  25971  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcobr  25983  dvcobrOLD  25984  dvnfre  25990  dvmptres2  26000  dvmptntr  26009  dvcnvlem  26014  dvcnv  26015  dvferm1lem  26022  dvferm2lem  26024  dvlip  26032  dvlipcn  26033  dvlip2  26034  c1liplem1  26035  dvgt0lem1  26041  lhop1lem  26052  lhop  26055  dvcnvrelem1  26056  dvcnvrelem2  26057  dvcnvre  26058  dvfsumle  26060  dvfsumleOLD  26061  dvfsumge  26062  dvfsumabs  26063  ftc1lem1  26076  ftc1lem2  26077  ftc1a  26078  ftc1lem4  26080  ftc2ditglem  26086  itgsubstlem  26089  ig1peu  26214  ig1pdvds  26219  taylfvallem1  26398  tayl0  26403  taylply2  26409  taylply2OLD  26410  taylply  26411  dvtaylp  26412  dvntaylp  26413  dvntaylp0  26414  taylthlem1  26415  ulmdvlem1  26443  ulmdvlem3  26445  psercn  26470  pserdvlem2  26472  abelth  26485  xrlimcnp  27011  lgamucov  27081  wilthlem2  27112  sqff1o  27225  chtublem  27255  pntlemq  27645  pntlemf  27649  sssslt1  27840  sssslt2  27841  scutbdaybnd  27860  scutbdaybnd2  27861  cofss  27964  coiniss  27965  tglineintmo  28650  ttgcontlem1  28899  pthdlem1  29786  shintcli  31348  shub1  31401  mdslmd1lem1  32344  mdexchi  32354  chirredlem1  32409  mdsymlem5  32426  sumdmdii  32434  sumdmdlem2  32438  fnpreimac  32681  fsuppinisegfi  32696  xrsupssd  32763  xrge0infssd  32765  swrdrn3  32940  swrdf1  32941  swrdrndisj  32942  pwrssmgc  32990  xrge0tsmsd  33065  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  fldgenss  33318  fldgenssp  33320  linds2eq  33409  elrspunidl  33456  ssdifidllem  33484  ssdifidlprm  33486  mxidlprm  33498  ssmxidllem  33501  ssmxidl  33502  qsdrnglem2  33524  rprmdvdsprod  33562  resssra  33638  lsssra  33639  exsslsb  33647  lbsdiflsp0  33677  dimkerim  33678  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  dimlssid  33683  fldextrspunlsplem  33723  fldextrspunlsp  33724  fldextrspunlem1  33725  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  constr01  33783  constrmon  33785  constrextdg2lem  33789  smatrcl  33795  locfinreflem  33839  cmpcref  33849  zarclsun  33869  zarclsiin  33870  zarclssn  33872  zarcmplem  33880  pnfneige0  33950  esum2d  34094  insiga  34138  sssigagen2  34147  dynkin  34168  dya2iocnei  34284  omsmon  34300  carsgclctunlem1  34319  carsggect  34320  omsmeas  34325  ftc2re  34613  fdvneggt  34615  fdvnegge  34617  reprsuc  34630  reprss  34632  reprlt  34634  reprinfz1  34637  logdivsqrle  34665  hgt750lemb  34671  bnj906  34944  bnj1020  34979  bnj1137  35009  bnj1408  35050  bnj1452  35066  erdszelem7  35202  erdszelem8  35203  erdsze2lem1  35208  connpconn  35240  cvmliftmolem1  35286  cvmlift2lem1  35307  cvmlift2lem9  35316  cvmlift2lem10  35317  cvmlift3lem6  35329  cvmlift3lem7  35330  satfsschain  35369  ss2mcls  35573  neibastop2lem  36361  fnemeet2  36368  fnejoin1  36369  ontgval  36432  unbdqndv1  36509  opnmbllem0  37663  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  sstotbnd2  37781  heiborlem1  37818  heiborlem8  37825  intidl  38036  lsmsat  39009  lssats  39013  lpssat  39014  lssatle  39016  lssat  39017  lsatcvatlem  39050  paddss12  39821  paddasslem17  39838  pmodlem1  39848  pmod1i  39850  pmodl42N  39853  elpcliN  39895  pclfinN  39902  polcon3N  39919  polcon2N  39921  paddunN  39929  pclfinclN  39952  poml5N  39956  osumcllem1N  39958  osumcllem2N  39959  osumcllem3N  39960  pl42lem2N  39982  pl42lem4N  39984  cdlemn5pre  41202  dihord1  41220  dihord2a  41221  dihord2b  41222  dihord5b  41261  dochss  41367  dochdmj1  41392  djhsumss  41409  djhunssN  41411  dochexmidlem2  41463  lclkrslem1  41539  lclkrslem2  41540  lcfrlem2  41545  aks4d1p4  42080  aks4d1p5  42081  aks4d1p7  42084  aks4d1p8  42088  aks6d1c2  42131  sticksstones1  42147  unitscyglem5  42200  prjcrv0  42643  elrfi  42705  ismrcd1  42709  istopclsd  42711  mrefg2  42718  aomclem2  43067  aomclem6  43071  hbtlem6  43141  hbt  43142  oege2  43320  cantnftermord  43333  omabs2  43345  tfsconcat0b  43359  naddgeoa  43407  naddwordnexlem0  43409  naddwordnexlem1  43410  dfno2  43441  mptrcllem  43626  dfrcl2  43687  relexp0a  43729  trclimalb2  43739  frege81d  43760  k0004ss2  44165  imo72b2lem2  44180  imo72b2  44185  uzwo4  45058  ssin0  45060  ixpssmapc  45078  ssinc  45092  ssdec  45093  supxrre3  45336  uzfissfz  45337  ssuzfz  45360  supminfxr  45475  inficc  45547  ressiocsup  45567  ressioosup  45568  ressiooinf  45570  limccog  45635  limclner  45666  limsupres  45720  limsupresuz2  45724  limsupequzlem  45737  supcnvlimsup  45755  limsupgtlem  45792  liminfresuz2  45802  cncfmptssg  45886  cncfuni  45901  icccncfext  45902  dvresntr  45933  dvbdfbdioolem1  45943  dvdmsscn  45951  dvnxpaek  45957  dvnprodlem2  45962  stoweidlem59  46074  fourierdlem20  46142  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem52  46173  fourierdlem58  46179  fourierdlem64  46185  fourierdlem73  46194  fourierdlem76  46197  fourierdlem80  46201  fourierdlem84  46205  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  fourierdlem113  46234  etransclem18  46267  ioorrnopnlem  46319  salincl  46339  intsal  46345  fsumlesge0  46392  sge0cl  46396  sge0supre  46404  sge0less  46407  sge0split  46424  sge0seq  46461  caragensspw  46524  omessre  46525  caragendifcl  46529  caratheodorylem1  46541  0ome  46544  omess0  46549  caragencmpl  46550  hoicvr  46563  hoissrrn  46564  hoicvrrex  46571  ovnlecvr  46573  ovnsslelem  46575  ovnssle  46576  ovnsubaddlem1  46585  hoissrrn2  46593  hoidmv1lelem1  46606  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem4  46613  ovnlecvr2  46625  voncmpl  46636  hspmbl  46644  opnvonmbllem1  46647  ovolval5lem2  46668  ovolval5lem3  46669  vonioolem1  46695  pimdecfgtioc  46730  pimincfltioc  46731  pimdecfgtioo  46732  pimincfltioo  46733  issmflem  46742  cnfsmf  46755  incsmflem  46756  smfsssmf  46758  smfadd  46780  decsmflem  46781  smflim  46792  smfres  46805  smfmul  46810  smfpimbor1lem1  46813  smfco  46817  smfsuplem1  46826  smfsuplem3  46828  smflimsuplem1  46835  smflimsuplem4  46838  smflimsuplem7  46841  cnneiima  48814  seposep  48823  iscnrm3rlem4  48840  iscnrm3llem1  48846  lubsscl  48857  glbsscl  48858  toplatglb  48890  setrecsss  49220  elpglem1  49230