Theorem sstrd 3927

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

Syntax hints:   → wi 4   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sstrid  3928  sstrdi  3929  rabssrabd  4012  ssdif2d  4074  uniintsn  4915  funss  6437  fssxp  6612  knatar  7208  tfisi  7680  suppssov1  7985  suppssfv  7989  tposss  8014  frrlem8  8080  tfrlem1  8178  omwordri  8365  oewordri  8385  oeeui  8395  oaabs2  8439  omopthlem1  8449  ecinxp  8539  sbthlem1  8823  dffi2  9112  hartogslem1  9231  cantnfcl  9355  cantnflt  9360  cantnfp1lem3  9368  cantnflem3  9379  cnfcom  9388  cnfcom3lem  9391  dftrpred3g  9412  rankssb  9537  tskwe  9639  dfac12lem2  9831  dfac12lem3  9832  cfflb  9946  cfcof  9961  ssfin2  10007  hsmexlem4  10116  ttukeylem6  10201  ttukeylem7  10202  fpwwe2lem1  10318  fpwwe2lem7  10324  fpwwe2lem10  10327  fpwwe2lem11  10328  canthnumlem  10335  canthwelem  10337  canthwe  10338  canthp1lem2  10340  pwfseqlem5  10350  wunex2  10425  tsktrss  10448  inttsk  10461  uzwo3  12612  supicc  13162  supiccub  13163  supicclub  13164  ssfzunsnext  13230  seqsplit  13684  seqf1olem2a  13689  seqz  13699  swrdval2  14287  trrelssd  14612  rtrclreclem4  14700  sumss  15364  qshash  15467  incexc  15477  incexc2  15478  prodss  15585  rpnnen2lem11  15861  vdwlem1  16610  ramub1lem1  16655  imasaddvallem  17157  imasvscaf  17167  mrerintcl  17223  ismred2  17229  mremre  17230  mrcuni  17247  mressmrcd  17253  submrc  17254  mrissmrid  17267  mreexexlem2d  17271  isacs2  17279  isacs1i  17283  invss  17390  ssctr  17454  funcres2b  17528  isacs3lem  18175  acsfiindd  18186  acsmapd  18187  acsmap2d  18188  tsrdir  18237  subsubm  18370  gsumwspan  18400  subsubg  18693  subgint  18694  cntzidss  18859  symggen  18993  pmtrdifellem1  18999  pmtrdifellem2  19000  pgpssslw  19134  lsmless1x  19164  lsmless2x  19165  lsmless12  19182  subglsm  19194  gsumval3lem2  19422  gsumzaddlem  19437  gsumzadd  19438  gsum2d  19488  dmdprdd  19517  dprdfeq0  19540  dprdspan  19545  dprdres  19546  dprdss  19547  dprdz  19548  subgdmdprd  19552  subgdprd  19553  dprdsn  19554  dprd2dlem1  19559  dprd2da  19560  dmdprdsplit2lem  19563  dprdsplit  19566  pgpfac1lem2  19593  pgpfac1lem3  19595  pgpfac1lem5  19597  subsubrg  19965  subdrgint  19986  lspss  20161  lspun  20164  lsslsp  20192  lmhmlsp  20226  lsmelval2  20262  lsmssspx  20265  lsppratlem2  20325  lsppratlem3  20326  lsppratlem4  20327  lbsextlem2  20336  lbsextlem3  20337  ocvlsp  20793  cssmre  20810  obselocv  20845  obslbs  20847  aspss  20991  mhpaddcl  21251  mhpinvcl  21252  mhpvscacl  21254  toponmre  22152  neiint  22163  neiss  22168  lpss  22201  lpss3  22203  restopnb  22234  restfpw  22238  neitr  22239  restcls  22240  restntr  22241  restlp  22242  ordtbas  22251  pnfnei  22279  mnfnei  22280  iscnp4  22322  cnclsi  22331  isreg2  22436  discmp  22457  cmpcld  22461  uncmp  22462  sscmp  22464  hauscmplem  22465  cmpfi  22467  iunconnlem  22486  clsconn  22489  2ndcctbss  22514  restnlly  22541  llyrest  22544  nllyrest  22545  llyidm  22547  nllyidm  22548  cldllycmp  22554  dislly  22556  comppfsc  22591  llycmpkgen2  22609  ptbasfi  22640  txnlly  22696  txcmplem1  22700  tx1stc  22709  xkococnlem  22718  qtopval2  22755  basqtop  22770  tgqtop  22771  qtoprest  22776  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  fsubbas  22926  fgabs  22938  fbasrn  22943  trfil2  22946  trfg  22950  isufil2  22967  trufil  22969  ssufl  22977  ufileu  22978  filufint  22979  fmfnfmlem4  23016  fmfnfm  23017  flimss2  23031  flimss1  23032  fclsfnflim  23086  flimfnfcls  23087  fclscmp  23089  cnpfcfi  23099  alexsubALT  23110  clssubg  23168  clsnsg  23169  tsmsres  23203  ustexsym  23275  ustex2sym  23276  ustex3sym  23277  ustneism  23283  trust  23289  utoptop  23294  restutopopn  23298  utop2nei  23310  utopreg  23312  cfiluweak  23355  neipcfilu  23356  blssps  23485  blss  23486  blcld  23567  blsscls  23569  met1stc  23583  met2ndci  23584  metust  23620  cfilucfil  23621  restmetu  23632  tgqioo  23869  xrsblre  23880  reconnlem2  23896  xrge0gsumle  23902  xrge0tsms  23903  rescncf  23966  cnmpopc  23997  cnheibor  24024  cnllycmp  24025  lebnum  24033  phtpycn  24052  cfilfcls  24343  iscmet3lem2  24361  cmetss  24385  cncmet  24391  bcthlem4  24396  bcth3  24400  rrxcph  24461  rrxmetlem  24476  minveclem4a  24499  minveclem4  24501  ivthicc  24527  ovollb  24548  ovollb2lem  24557  ovollb2  24558  nulmbl2  24605  ioorcl2  24641  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  opnmbllem  24670  volcn  24675  volivth  24676  mbfeqalem1  24710  itg10a  24780  mbfi1fseqlem4  24788  ditgcl  24927  ditgswap  24928  ditgsplitlem  24929  limcflf  24950  limcres  24955  dvbss  24970  dvbsss  24971  perfdvf  24972  dvreslem  24978  dvres2lem  24979  dvres3  24982  dvmptresicc  24985  dvcnp  24988  dvcnp2  24989  dvcn  24990  dvnff  24992  dvn2bss  24999  dvnres  25000  cpnord  25004  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  dvnfre  25021  dvmptres2  25031  dvmptntr  25040  dvcnvlem  25045  dvcnv  25046  dvferm1lem  25053  dvferm2lem  25055  dvlip  25062  dvlipcn  25063  dvlip2  25064  c1liplem1  25065  dvgt0lem1  25071  lhop1lem  25082  lhop  25085  dvcnvrelem1  25086  dvcnvrelem2  25087  dvcnvre  25088  dvfsumle  25090  dvfsumge  25091  dvfsumabs  25092  ftc1lem1  25104  ftc1lem2  25105  ftc1a  25106  ftc1lem4  25108  ftc2ditglem  25114  itgsubstlem  25117  ig1peu  25241  ig1pdvds  25246  taylfvallem1  25421  tayl0  25426  taylply2  25432  taylply  25433  dvtaylp  25434  dvntaylp  25435  dvntaylp0  25436  taylthlem1  25437  ulmdvlem1  25464  ulmdvlem3  25466  psercn  25490  pserdvlem2  25492  abelth  25505  xrlimcnp  26023  lgamucov  26092  wilthlem2  26123  sqff1o  26236  chtublem  26264  pntlemq  26654  pntlemf  26658  tglineintmo  26907  ttgcontlem1  27155  pthdlem1  28035  shintcli  29592  shub1  29645  mdslmd1lem1  30588  mdexchi  30598  chirredlem1  30653  mdsymlem5  30670  sumdmdii  30678  sumdmdlem2  30682  fnpreimac  30910  fsuppinisegfi  30923  xrsupssd  30984  xrge0infssd  30986  swrdrn3  31129  swrdf1  31130  swrdrndisj  31131  pwrssmgc  31180  xrge0tsmsd  31219  linds2eq  31477  elrspunidl  31508  mxidlprm  31542  ssmxidllem  31543  ssmxidl  31544  lbsdiflsp0  31609  dimkerim  31610  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  smatrcl  31648  locfinreflem  31692  cmpcref  31702  zarclsun  31722  zarclsiin  31723  zarclssn  31725  zarcmplem  31733  pnfneige0  31803  esum2d  31961  insiga  32005  sssigagen2  32014  dynkin  32035  dya2iocnei  32149  omsmon  32165  carsgclctunlem1  32184  carsggect  32185  omsmeas  32190  ftc2re  32478  fdvneggt  32480  fdvnegge  32482  reprsuc  32495  reprss  32497  reprlt  32499  reprinfz1  32502  logdivsqrle  32530  hgt750lemb  32536  bnj906  32810  bnj1020  32845  bnj1137  32875  bnj1408  32916  bnj1452  32932  erdszelem7  33059  erdszelem8  33060  erdsze2lem1  33065  connpconn  33097  cvmliftmolem1  33143  cvmlift2lem1  33164  cvmlift2lem9  33173  cvmlift2lem10  33174  cvmlift3lem6  33186  cvmlift3lem7  33187  satfsschain  33226  ss2mcls  33430  ttrcltr  33702  sssslt1  33916  sssslt2  33917  scutbdaybnd  33936  scutbdaybnd2  33937  neibastop2lem  34476  fnemeet2  34483  fnejoin1  34484  ontgval  34547  unbdqndv1  34615  opnmbllem0  35740  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  sstotbnd2  35859  heiborlem1  35896  heiborlem8  35903  intidl  36114  lsmsat  36949  lssats  36953  lpssat  36954  lssatle  36956  lssat  36957  lsatcvatlem  36990  paddss12  37760  paddasslem17  37777  pmodlem1  37787  pmod1i  37789  pmodl42N  37792  elpcliN  37834  pclfinN  37841  polcon3N  37858  polcon2N  37860  paddunN  37868  pclfinclN  37891  poml5N  37895  osumcllem1N  37897  osumcllem2N  37898  osumcllem3N  37899  pl42lem2N  37921  pl42lem4N  37923  cdlemn5pre  39141  dihord1  39159  dihord2a  39160  dihord2b  39161  dihord5b  39200  dochss  39306  dochdmj1  39331  djhsumss  39348  djhunssN  39350  dochexmidlem2  39402  lclkrslem1  39478  lclkrslem2  39479  lcfrlem2  39484  aks4d1p4  40015  aks4d1p5  40016  aks4d1p7  40019  aks4d1p8  40023  sticksstones1  40030  elrfi  40432  ismrcd1  40436  istopclsd  40438  mrefg2  40445  aomclem2  40796  aomclem6  40800  hbtlem6  40870  hbt  40871  mptrcllem  41110  dfrcl2  41171  relexp0a  41213  trclimalb2  41223  frege81d  41244  k0004ss2  41651  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2  41672  uzwo4  42490  ssin0  42492  ixpssmapc  42511  ssinc  42526  ssdec  42527  supxrre3  42754  uzfissfz  42755  ssuzfz  42778  supminfxr  42894  inficc  42962  ressiocsup  42982  ressioosup  42983  ressiooinf  42985  limccog  43051  limclner  43082  limsupres  43136  limsupresuz2  43140  limsupequzlem  43153  limsupvaluz2  43169  supcnvlimsup  43171  limsupgtlem  43208  liminfresuz2  43218  cncfmptssg  43302  cncfuni  43317  icccncfext  43318  dvresntr  43349  dvbdfbdioolem1  43359  dvdmsscn  43367  dvnxpaek  43373  dvnprodlem2  43378  stoweidlem59  43490  fourierdlem20  43558  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem52  43589  fourierdlem58  43595  fourierdlem64  43601  fourierdlem73  43610  fourierdlem76  43613  fourierdlem80  43617  fourierdlem84  43621  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  fourierdlem113  43650  etransclem18  43683  ioorrnopnlem  43735  salincl  43754  intsal  43759  fsumlesge0  43805  sge0cl  43809  sge0supre  43817  sge0less  43820  sge0split  43837  sge0seq  43874  caragensspw  43937  omessre  43938  caragendifcl  43942  caratheodorylem1  43954  0ome  43957  omess0  43962  caragencmpl  43963  hoicvr  43976  hoissrrn  43977  hoicvrrex  43984  ovnlecvr  43986  ovnsslelem  43988  ovnssle  43989  ovnsubaddlem1  43998  hoissrrn2  44006  hoidmv1lelem1  44019  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem4  44026  ovnlecvr2  44038  voncmpl  44049  hspmbl  44057  opnvonmbllem1  44060  ovolval5lem2  44081  ovolval5lem3  44082  vonioolem1  44108  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  issmflem  44150  cnfsmf  44163  incsmflem  44164  smfsssmf  44166  smfadd  44187  decsmflem  44188  smflim  44199  smfres  44211  smfmul  44216  smfpimbor1lem1  44219  smfco  44223  smfsuplem1  44231  smfsuplem3  44233  smflimsuplem1  44240  smflimsuplem4  44243  smflimsuplem7  44246  subsubmgm  45239  cnneiima  46098  seposep  46107  iscnrm3rlem4  46125  iscnrm3llem1  46131  lubsscl  46142  glbsscl  46143  toplatglb  46175  setrecsss  46292  elpglem1  46302