Theorem sstrd 3911

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

Syntax hints:   → wi 4   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  sstrid  3912  sstrdi  3913  rabssrabd  3996  ssdif2d  4058  uniintsn  4898  funss  6399  fssxp  6573  knatar  7166  tfisi  7637  suppssov1  7940  suppssfv  7944  tposss  7969  frrlem8  8034  tfrlem1  8112  omwordri  8300  oewordri  8320  oeeui  8330  oaabs2  8374  omopthlem1  8384  ecinxp  8474  sbthlem1  8756  dffi2  9039  hartogslem1  9158  cantnfcl  9282  cantnflt  9287  cantnfp1lem3  9295  cantnflem3  9306  cnfcom  9315  cnfcom3lem  9318  dftrpred3g  9339  rankssb  9464  tskwe  9566  dfac12lem2  9758  dfac12lem3  9759  cfflb  9873  cfcof  9888  ssfin2  9934  hsmexlem4  10043  ttukeylem6  10128  ttukeylem7  10129  fpwwe2lem1  10245  fpwwe2lem7  10251  fpwwe2lem10  10254  fpwwe2lem11  10255  canthnumlem  10262  canthwelem  10264  canthwe  10265  canthp1lem2  10267  pwfseqlem5  10277  wunex2  10352  tsktrss  10375  inttsk  10388  uzwo3  12539  supicc  13089  supiccub  13090  supicclub  13091  ssfzunsnext  13157  seqsplit  13609  seqf1olem2a  13614  seqz  13624  swrdval2  14211  trrelssd  14536  rtrclreclem4  14624  sumss  15288  qshash  15391  incexc  15401  incexc2  15402  prodss  15509  rpnnen2lem11  15785  vdwlem1  16534  ramub1lem1  16579  imasaddvallem  17034  imasvscaf  17044  mrerintcl  17100  ismred2  17106  mremre  17107  mrcuni  17124  mressmrcd  17130  submrc  17131  mrissmrid  17144  mreexexlem2d  17148  isacs2  17156  isacs1i  17160  invss  17266  ssctr  17330  funcres2b  17403  isacs3lem  18048  acsfiindd  18059  acsmapd  18060  acsmap2d  18061  tsrdir  18110  subsubm  18243  gsumwspan  18273  subsubg  18566  subgint  18567  cntzidss  18732  symggen  18862  pmtrdifellem1  18868  pmtrdifellem2  18869  pgpssslw  19003  lsmless1x  19033  lsmless2x  19034  lsmless12  19051  subglsm  19063  gsumval3lem2  19291  gsumzaddlem  19306  gsumzadd  19307  gsum2d  19357  dmdprdd  19386  dprdfeq0  19409  dprdspan  19414  dprdres  19415  dprdss  19416  dprdz  19417  subgdmdprd  19421  subgdprd  19422  dprdsn  19423  dprd2dlem1  19428  dprd2da  19429  dmdprdsplit2lem  19432  dprdsplit  19435  pgpfac1lem2  19462  pgpfac1lem3  19464  pgpfac1lem5  19466  subsubrg  19826  subdrgint  19847  lspss  20021  lspun  20024  lsslsp  20052  lmhmlsp  20086  lsmelval2  20122  lsmssspx  20125  lsppratlem2  20185  lsppratlem3  20186  lsppratlem4  20187  lbsextlem2  20196  lbsextlem3  20197  ocvlsp  20638  cssmre  20655  obselocv  20690  obslbs  20692  aspss  20836  mhpaddcl  21091  mhpinvcl  21092  mhpvscacl  21094  toponmre  21990  neiint  22001  neiss  22006  lpss  22039  lpss3  22041  restopnb  22072  restfpw  22076  neitr  22077  restcls  22078  restntr  22079  restlp  22080  ordtbas  22089  pnfnei  22117  mnfnei  22118  iscnp4  22160  cnclsi  22169  isreg2  22274  discmp  22295  cmpcld  22299  uncmp  22300  sscmp  22302  hauscmplem  22303  cmpfi  22305  iunconnlem  22324  clsconn  22327  2ndcctbss  22352  restnlly  22379  llyrest  22382  nllyrest  22383  llyidm  22385  nllyidm  22386  cldllycmp  22392  dislly  22394  comppfsc  22429  llycmpkgen2  22447  ptbasfi  22478  txnlly  22534  txcmplem1  22538  tx1stc  22547  xkococnlem  22556  qtopval2  22593  basqtop  22608  tgqtop  22609  qtoprest  22614  kqreglem1  22638  kqreglem2  22639  kqnrmlem1  22640  kqnrmlem2  22641  fsubbas  22764  fgabs  22776  fbasrn  22781  trfil2  22784  trfg  22788  isufil2  22805  trufil  22807  ssufl  22815  ufileu  22816  filufint  22817  fmfnfmlem4  22854  fmfnfm  22855  flimss2  22869  flimss1  22870  fclsfnflim  22924  flimfnfcls  22925  fclscmp  22927  cnpfcfi  22937  alexsubALT  22948  clssubg  23006  clsnsg  23007  tsmsres  23041  ustexsym  23113  ustex2sym  23114  ustex3sym  23115  ustneism  23121  trust  23127  utoptop  23132  restutopopn  23136  utop2nei  23148  utopreg  23150  cfiluweak  23192  neipcfilu  23193  blssps  23322  blss  23323  blcld  23403  blsscls  23405  met1stc  23419  met2ndci  23420  metust  23456  cfilucfil  23457  restmetu  23468  tgqioo  23697  xrsblre  23708  reconnlem2  23724  xrge0gsumle  23730  xrge0tsms  23731  rescncf  23794  cnmpopc  23825  cnheibor  23852  cnllycmp  23853  lebnum  23861  phtpycn  23880  cfilfcls  24171  iscmet3lem2  24189  cmetss  24213  cncmet  24219  bcthlem4  24224  bcth3  24228  rrxcph  24289  rrxmetlem  24304  minveclem4a  24327  minveclem4  24329  ivthicc  24355  ovollb  24376  ovollb2lem  24385  ovollb2  24386  nulmbl2  24433  ioorcl2  24469  uniioombllem3  24482  uniioombllem4  24483  uniioombllem5  24484  opnmbllem  24498  volcn  24503  volivth  24504  mbfeqalem1  24538  itg10a  24608  mbfi1fseqlem4  24616  ditgcl  24755  ditgswap  24756  ditgsplitlem  24757  limcflf  24778  limcres  24783  dvbss  24798  dvbsss  24799  perfdvf  24800  dvreslem  24806  dvres2lem  24807  dvres3  24810  dvmptresicc  24813  dvcnp  24816  dvcnp2  24817  dvcn  24818  dvnff  24820  dvn2bss  24827  dvnres  24828  cpnord  24832  dvaddbr  24835  dvmulbr  24836  dvcobr  24843  dvnfre  24849  dvmptres2  24859  dvmptntr  24868  dvcnvlem  24873  dvcnv  24874  dvferm1lem  24881  dvferm2lem  24883  dvlip  24890  dvlipcn  24891  dvlip2  24892  c1liplem1  24893  dvgt0lem1  24899  lhop1lem  24910  lhop  24913  dvcnvrelem1  24914  dvcnvrelem2  24915  dvcnvre  24916  dvfsumle  24918  dvfsumge  24919  dvfsumabs  24920  ftc1lem1  24932  ftc1lem2  24933  ftc1a  24934  ftc1lem4  24936  ftc2ditglem  24942  itgsubstlem  24945  ig1peu  25069  ig1pdvds  25074  taylfvallem1  25249  tayl0  25254  taylply2  25260  taylply  25261  dvtaylp  25262  dvntaylp  25263  dvntaylp0  25264  taylthlem1  25265  ulmdvlem1  25292  ulmdvlem3  25294  psercn  25318  pserdvlem2  25320  abelth  25333  xrlimcnp  25851  lgamucov  25920  wilthlem2  25951  sqff1o  26064  chtublem  26092  pntlemq  26482  pntlemf  26486  tglineintmo  26733  ttgcontlem1  26976  pthdlem1  27853  shintcli  29410  shub1  29463  mdslmd1lem1  30406  mdexchi  30416  chirredlem1  30471  mdsymlem5  30488  sumdmdii  30496  sumdmdlem2  30500  fnpreimac  30728  fsuppinisegfi  30741  xrsupssd  30802  xrge0infssd  30804  swrdrn3  30947  swrdf1  30948  swrdrndisj  30949  pwrssmgc  30997  xrge0tsmsd  31036  linds2eq  31289  elrspunidl  31320  mxidlprm  31354  ssmxidllem  31355  ssmxidl  31356  lbsdiflsp0  31421  dimkerim  31422  fedgmullem1  31424  fedgmullem2  31425  fedgmul  31426  smatrcl  31460  locfinreflem  31504  cmpcref  31514  zarclsun  31534  zarclsiin  31535  zarclssn  31537  zarcmplem  31545  pnfneige0  31615  esum2d  31773  insiga  31817  sssigagen2  31826  dynkin  31847  dya2iocnei  31961  omsmon  31977  carsgclctunlem1  31996  carsggect  31997  omsmeas  32002  ftc2re  32290  fdvneggt  32292  fdvnegge  32294  reprsuc  32307  reprss  32309  reprlt  32311  reprinfz1  32314  logdivsqrle  32342  hgt750lemb  32348  bnj906  32623  bnj1020  32658  bnj1137  32688  bnj1408  32729  bnj1452  32745  erdszelem7  32872  erdszelem8  32873  erdsze2lem1  32878  connpconn  32910  cvmliftmolem1  32956  cvmlift2lem1  32977  cvmlift2lem9  32986  cvmlift2lem10  32987  cvmlift3lem6  32999  cvmlift3lem7  33000  satfsschain  33039  ss2mcls  33243  ttrcltr  33515  sssslt1  33726  sssslt2  33727  scutbdaybnd  33746  scutbdaybnd2  33747  neibastop2lem  34286  fnemeet2  34293  fnejoin1  34294  ontgval  34357  unbdqndv1  34425  opnmbllem0  35550  ftc1anclem7  35593  ftc1anclem8  35594  ftc1anc  35595  sstotbnd2  35669  heiborlem1  35706  heiborlem8  35713  intidl  35924  lsmsat  36759  lssats  36763  lpssat  36764  lssatle  36766  lssat  36767  lsatcvatlem  36800  paddss12  37570  paddasslem17  37587  pmodlem1  37597  pmod1i  37599  pmodl42N  37602  elpcliN  37644  pclfinN  37651  polcon3N  37668  polcon2N  37670  paddunN  37678  pclfinclN  37701  poml5N  37705  osumcllem1N  37707  osumcllem2N  37708  osumcllem3N  37709  pl42lem2N  37731  pl42lem4N  37733  cdlemn5pre  38951  dihord1  38969  dihord2a  38970  dihord2b  38971  dihord5b  39010  dochss  39116  dochdmj1  39141  djhsumss  39158  djhunssN  39160  dochexmidlem2  39212  lclkrslem1  39288  lclkrslem2  39289  lcfrlem2  39294  sticksstones1  39824  elrfi  40219  ismrcd1  40223  istopclsd  40225  mrefg2  40232  aomclem2  40583  aomclem6  40587  hbtlem6  40657  hbt  40658  mptrcllem  40897  dfrcl2  40959  relexp0a  41001  trclimalb2  41011  frege81d  41032  k0004ss2  41439  imo72b2lem0  41453  imo72b2lem2  41455  imo72b2  41461  uzwo4  42274  ssin0  42276  ixpssmapc  42295  ssinc  42310  ssdec  42311  supxrre3  42537  uzfissfz  42538  ssuzfz  42561  supminfxr  42679  inficc  42747  ressiocsup  42767  ressioosup  42768  ressiooinf  42770  limccog  42836  limclner  42867  limsupres  42921  limsupresuz2  42925  limsupequzlem  42938  limsupvaluz2  42954  supcnvlimsup  42956  limsupgtlem  42993  liminfresuz2  43003  cncfmptssg  43087  cncfuni  43102  icccncfext  43103  dvresntr  43134  dvbdfbdioolem1  43144  dvdmsscn  43152  dvnxpaek  43158  dvnprodlem2  43163  stoweidlem59  43275  fourierdlem20  43343  fourierdlem42  43365  fourierdlem48  43370  fourierdlem49  43371  fourierdlem52  43374  fourierdlem58  43380  fourierdlem64  43386  fourierdlem73  43395  fourierdlem76  43398  fourierdlem80  43402  fourierdlem84  43406  fourierdlem93  43415  fourierdlem103  43425  fourierdlem104  43426  fourierdlem113  43435  etransclem18  43468  ioorrnopnlem  43520  salincl  43539  intsal  43544  fsumlesge0  43590  sge0cl  43594  sge0supre  43602  sge0less  43605  sge0split  43622  sge0seq  43659  caragensspw  43722  omessre  43723  caragendifcl  43727  caratheodorylem1  43739  0ome  43742  omess0  43747  caragencmpl  43748  hoicvr  43761  hoissrrn  43762  hoicvrrex  43769  ovnlecvr  43771  ovnsslelem  43773  ovnssle  43774  ovnsubaddlem1  43783  hoissrrn2  43791  hoidmv1lelem1  43804  hoidmvlelem1  43808  hoidmvlelem2  43809  hoidmvlelem4  43811  ovnlecvr2  43823  voncmpl  43834  hspmbl  43842  opnvonmbllem1  43845  ovolval5lem2  43866  ovolval5lem3  43867  vonioolem1  43893  pimdecfgtioc  43924  pimincfltioc  43925  pimdecfgtioo  43926  pimincfltioo  43927  issmflem  43935  cnfsmf  43948  incsmflem  43949  smfsssmf  43951  smfadd  43972  decsmflem  43973  smflim  43984  smfres  43996  smfmul  44001  smfpimbor1lem1  44004  smfco  44008  smfsuplem1  44016  smfsuplem3  44018  smflimsuplem1  44025  smflimsuplem4  44028  smflimsuplem7  44031  subsubmgm  45024  cnneiima  45883  seposep  45892  iscnrm3rlem4  45910  iscnrm3llem1  45916  lubsscl  45927  glbsscl  45928  toplatglb  45960  setrecsss  46077  elpglem1  46087