Theorem sstrd 3941

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

Syntax hints:   → wi 4   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3915

This theorem is referenced by:  sstrid  3942  sstrdi  3943  rabssrabd  4032  ssdif2d  4097  uniintsn  4935  funss  6505  fssxp  6683  knatar  7297  tfisi  7795  suppssov1  8133  suppssov2  8134  suppssfv  8138  tposss  8163  frrlem8  8229  tfrlem1  8301  omwordri  8493  oewordri  8513  oeeui  8523  oaabs2  8570  omopthlem1  8580  ecinxp  8722  sbthlem1  9007  dffi2  9314  hartogslem1  9435  cantnfcl  9564  cantnflt  9569  cantnfp1lem3  9577  cantnflem3  9588  cnfcom  9597  cnfcom3lem  9600  ttrcltr  9613  rankssb  9748  tskwe  9850  dfac12lem2  10043  dfac12lem3  10044  cfflb  10157  cfcof  10172  ssfin2  10218  hsmexlem4  10327  ttukeylem6  10412  ttukeylem7  10413  fpwwe2lem1  10529  fpwwe2lem7  10535  fpwwe2lem10  10538  fpwwe2lem11  10539  canthnumlem  10546  canthwelem  10548  canthwe  10549  canthp1lem2  10551  pwfseqlem5  10561  wunex2  10636  tsktrss  10659  inttsk  10672  uzwo3  12843  xrsupssd  13234  supicc  13403  supiccub  13404  supicclub  13405  ssfzunsnext  13471  seqsplit  13944  seqf1olem2a  13949  seqz  13959  swrdval2  14556  trrelssd  14882  rtrclreclem4  14970  sumss  15633  qshash  15736  incexc  15746  incexc2  15747  prodss  15856  rpnnen2lem11  16135  vdwlem1  16895  ramub1lem1  16940  imasaddvallem  17435  imasvscaf  17445  mrerintcl  17501  ismred2  17507  mremre  17508  mrcuni  17529  mressmrcd  17535  submrc  17536  mrissmrid  17549  mreexexlem2d  17553  isacs2  17561  isacs1i  17565  invss  17670  ssctr  17734  funcres2b  17806  isacs3lem  18450  acsfiindd  18461  acsmapd  18462  acsmap2d  18463  tsrdir  18512  subsubmgm  18620  subsubm  18726  gsumwspan  18756  subsubg  19064  subgint  19065  cntzidss  19254  symggen  19384  pmtrdifellem1  19390  pmtrdifellem2  19391  pgpssslw  19528  lsmless1x  19558  lsmless2x  19559  lsmless12  19576  subglsm  19587  gsumval3lem2  19820  gsumzaddlem  19835  gsumzadd  19836  gsum2d  19886  dmdprdd  19915  dprdfeq0  19938  dprdspan  19943  dprdres  19944  dprdss  19945  dprdz  19946  subgdmdprd  19950  subgdprd  19951  dprdsn  19952  dprd2dlem1  19957  dprd2da  19958  dmdprdsplit2lem  19961  dprdsplit  19964  pgpfac1lem2  19991  pgpfac1lem3  19993  pgpfac1lem5  19995  subsubrng  20480  subsubrg  20515  subdrgint  20720  lspss  20919  lspun  20922  lsslsp  20950  lsslspOLD  20951  lmhmlsp  20985  lsmelval2  21021  lsmssspx  21024  lsppratlem2  21087  lsppratlem3  21088  lsppratlem4  21089  lbsextlem2  21098  lbsextlem3  21099  ocvlsp  21615  cssmre  21632  obselocv  21667  obslbs  21669  aspss  21816  mhpaddcl  22067  mhpinvcl  22068  mhpvscacl  22070  psdmullem  22081  toponmre  23009  neiint  23020  neiss  23025  lpss  23058  lpss3  23060  restopnb  23091  restfpw  23095  neitr  23096  restcls  23097  restntr  23098  restlp  23099  ordtbas  23108  pnfnei  23136  mnfnei  23137  iscnp4  23179  cnclsi  23188  isreg2  23293  discmp  23314  cmpcld  23318  uncmp  23319  sscmp  23321  hauscmplem  23322  cmpfi  23324  iunconnlem  23343  clsconn  23346  2ndcctbss  23371  restnlly  23398  llyrest  23401  nllyrest  23402  llyidm  23404  nllyidm  23405  cldllycmp  23411  dislly  23413  comppfsc  23448  llycmpkgen2  23466  ptbasfi  23497  txnlly  23553  txcmplem1  23557  tx1stc  23566  xkococnlem  23575  qtopval2  23612  basqtop  23627  tgqtop  23628  qtoprest  23633  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  fsubbas  23783  fgabs  23795  fbasrn  23800  trfil2  23803  trfg  23807  isufil2  23824  trufil  23826  ssufl  23834  ufileu  23835  filufint  23836  fmfnfmlem4  23873  fmfnfm  23874  flimss2  23888  flimss1  23889  fclsfnflim  23943  flimfnfcls  23944  fclscmp  23946  cnpfcfi  23956  alexsubALT  23967  clssubg  24025  clsnsg  24026  tsmsres  24060  ustexsym  24132  ustex2sym  24133  ustex3sym  24134  ustneism  24140  trust  24145  utoptop  24150  restutopopn  24154  utop2nei  24166  utopreg  24168  cfiluweak  24210  neipcfilu  24211  blssps  24340  blss  24341  blcld  24421  blsscls  24423  met1stc  24437  met2ndci  24438  metust  24474  cfilucfil  24475  restmetu  24486  tgqioo  24716  xrsblre  24728  reconnlem2  24744  xrge0gsumle  24750  xrge0tsms  24751  rescncf  24818  cnmpopc  24850  cnheibor  24882  cnllycmp  24883  lebnum  24891  phtpycn  24910  cfilfcls  25202  iscmet3lem2  25220  cmetss  25244  cncmet  25250  bcthlem4  25255  bcth3  25259  rrxcph  25320  rrxmetlem  25335  minveclem4a  25358  minveclem4  25360  ivthicc  25387  ovollb  25408  ovollb2lem  25417  ovollb2  25418  nulmbl2  25465  ioorcl2  25501  uniioombllem3  25514  uniioombllem4  25515  uniioombllem5  25516  opnmbllem  25530  volcn  25535  volivth  25536  mbfeqalem1  25570  itg10a  25639  mbfi1fseqlem4  25647  ditgcl  25787  ditgswap  25788  ditgsplitlem  25789  limcflf  25810  limcres  25815  dvbss  25830  dvbsss  25831  perfdvf  25832  dvreslem  25838  dvres2lem  25839  dvres3  25842  dvmptresicc  25845  dvcnp  25848  dvcnp2  25849  dvcnp2OLD  25850  dvcn  25851  dvnff  25853  dvn2bss  25860  dvnres  25861  cpnord  25865  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvcobr  25877  dvcobrOLD  25878  dvnfre  25884  dvmptres2  25894  dvmptntr  25903  dvcnvlem  25908  dvcnv  25909  dvferm1lem  25916  dvferm2lem  25918  dvlip  25926  dvlipcn  25927  dvlip2  25928  c1liplem1  25929  dvgt0lem1  25935  lhop1lem  25946  lhop  25949  dvcnvrelem1  25950  dvcnvrelem2  25951  dvcnvre  25952  dvfsumle  25954  dvfsumleOLD  25955  dvfsumge  25956  dvfsumabs  25957  ftc1lem1  25970  ftc1lem2  25971  ftc1a  25972  ftc1lem4  25974  ftc2ditglem  25980  itgsubstlem  25983  ig1peu  26108  ig1pdvds  26113  taylfvallem1  26292  tayl0  26297  taylply2  26303  taylply2OLD  26304  taylply  26305  dvtaylp  26306  dvntaylp  26307  dvntaylp0  26308  taylthlem1  26309  ulmdvlem1  26337  ulmdvlem3  26339  psercn  26364  pserdvlem2  26366  abelth  26379  xrlimcnp  26906  lgamucov  26976  wilthlem2  27007  sqff1o  27120  chtublem  27150  pntlemq  27540  pntlemf  27544  sssslt1  27737  sssslt2  27738  scutbdaybnd  27757  scutbdaybnd2  27758  eqscut3  27766  cofss  27875  coiniss  27876  tglineintmo  28621  ttgcontlem1  28864  pthdlem1  29746  shintcli  31311  shub1  31364  mdslmd1lem1  32307  mdexchi  32317  chirredlem1  32372  mdsymlem5  32389  sumdmdii  32397  sumdmdlem2  32401  fnpreimac  32655  fsuppinisegfi  32672  xrge0infssd  32748  swrdrn3  32943  swrdf1  32944  swrdrndisj  32945  pwrssmgc  32988  xrge0tsmsd  33049  elrgspnlem4  33219  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  fldgenss  33289  fldgenssp  33291  linds2eq  33353  elrspunidl  33400  ssdifidllem  33428  ssdifidlprm  33430  mxidlprm  33442  ssmxidllem  33445  ssmxidl  33446  qsdrnglem2  33468  rprmdvdsprod  33506  ressply1evls1  33535  resssra  33620  lsssra  33621  exsslsb  33630  lbsdiflsp0  33660  dimkerim  33661  fedgmullem1  33663  fedgmullem2  33664  fedgmul  33665  dimlssid  33666  fldextrspunlsplem  33707  fldextrspunlsp  33708  fldextrspunlem1  33709  fldextrspundgdvdslem  33714  fldextrspundgdvds  33715  constr01  33776  constrmon  33778  constrextdg2lem  33782  constrfiss  33785  smatrcl  33830  locfinreflem  33874  cmpcref  33884  zarclsun  33904  zarclsiin  33905  zarclssn  33907  zarcmplem  33915  pnfneige0  33985  esum2d  34127  insiga  34171  sssigagen2  34180  dynkin  34201  dya2iocnei  34316  omsmon  34332  carsgclctunlem1  34351  carsggect  34352  omsmeas  34357  ftc2re  34632  fdvneggt  34634  fdvnegge  34636  reprsuc  34649  reprss  34651  reprlt  34653  reprinfz1  34656  logdivsqrle  34684  hgt750lemb  34690  bnj906  34963  bnj1020  34998  bnj1137  35028  bnj1408  35069  bnj1452  35085  rankval4b  35132  fineqvnttrclselem2  35163  erdszelem7  35262  erdszelem8  35263  erdsze2lem1  35268  connpconn  35300  cvmliftmolem1  35346  cvmlift2lem1  35367  cvmlift2lem9  35376  cvmlift2lem10  35377  cvmlift3lem6  35389  cvmlift3lem7  35390  satfsschain  35429  ss2mcls  35633  neibastop2lem  36425  fnemeet2  36432  fnejoin1  36433  ontgval  36496  unbdqndv1  36573  opnmbllem0  37717  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  sstotbnd2  37835  heiborlem1  37872  heiborlem8  37879  intidl  38090  lsmsat  39128  lssats  39132  lpssat  39133  lssatle  39135  lssat  39136  lsatcvatlem  39169  paddss12  39939  paddasslem17  39956  pmodlem1  39966  pmod1i  39968  pmodl42N  39971  elpcliN  40013  pclfinN  40020  polcon3N  40037  polcon2N  40039  paddunN  40047  pclfinclN  40070  poml5N  40074  osumcllem1N  40076  osumcllem2N  40077  osumcllem3N  40078  pl42lem2N  40100  pl42lem4N  40102  cdlemn5pre  41320  dihord1  41338  dihord2a  41339  dihord2b  41340  dihord5b  41379  dochss  41485  dochdmj1  41510  djhsumss  41527  djhunssN  41529  dochexmidlem2  41581  lclkrslem1  41657  lclkrslem2  41658  lcfrlem2  41663  aks4d1p4  42193  aks4d1p5  42194  aks4d1p7  42197  aks4d1p8  42201  aks6d1c2  42244  sticksstones1  42260  unitscyglem5  42313  prjcrv0  42752  elrfi  42812  ismrcd1  42816  istopclsd  42818  mrefg2  42825  aomclem2  43173  aomclem6  43177  hbtlem6  43247  hbt  43248  oege2  43425  cantnftermord  43438  omabs2  43450  tfsconcat0b  43464  naddgeoa  43512  naddwordnexlem0  43514  naddwordnexlem1  43515  dfno2  43546  mptrcllem  43731  dfrcl2  43792  relexp0a  43834  trclimalb2  43844  frege81d  43865  k0004ss2  44270  imo72b2lem2  44285  imo72b2  44290  uzwo4  45175  ssin0  45177  ixpssmapc  45195  ssinc  45209  ssdec  45210  supxrre3  45449  uzfissfz  45450  ssuzfz  45473  supminfxr  45587  inficc  45659  ressiocsup  45679  ressioosup  45680  ressiooinf  45682  limccog  45745  limclner  45774  limsupres  45828  limsupresuz2  45832  limsupequzlem  45845  supcnvlimsup  45863  limsupgtlem  45900  liminfresuz2  45910  cncfmptssg  45994  cncfuni  46009  icccncfext  46010  dvresntr  46041  dvbdfbdioolem1  46051  dvdmsscn  46059  dvnxpaek  46065  dvnprodlem2  46070  stoweidlem59  46182  fourierdlem20  46250  fourierdlem42  46272  fourierdlem48  46277  fourierdlem49  46278  fourierdlem52  46281  fourierdlem58  46287  fourierdlem64  46293  fourierdlem73  46302  fourierdlem76  46305  fourierdlem80  46309  fourierdlem84  46313  fourierdlem93  46322  fourierdlem103  46332  fourierdlem104  46333  fourierdlem113  46342  etransclem18  46375  ioorrnopnlem  46427  salincl  46447  intsal  46453  fsumlesge0  46500  sge0cl  46504  sge0supre  46512  sge0less  46515  sge0split  46532  sge0seq  46569  caragensspw  46632  omessre  46633  caragendifcl  46637  caratheodorylem1  46649  0ome  46652  omess0  46657  caragencmpl  46658  hoicvr  46671  hoissrrn  46672  hoicvrrex  46679  ovnlecvr  46681  ovnsslelem  46683  ovnssle  46684  ovnsubaddlem1  46693  hoissrrn2  46701  hoidmv1lelem1  46714  hoidmvlelem1  46718  hoidmvlelem2  46719  hoidmvlelem4  46721  ovnlecvr2  46733  voncmpl  46744  hspmbl  46752  opnvonmbllem1  46755  ovolval5lem2  46776  ovolval5lem3  46777  vonioolem1  46803  pimdecfgtioc  46838  pimincfltioc  46839  pimdecfgtioo  46840  pimincfltioo  46841  issmflem  46850  cnfsmf  46863  incsmflem  46864  smfsssmf  46866  smfadd  46888  decsmflem  46889  smflim  46900  smfres  46913  smfmul  46918  smfpimbor1lem1  46921  smfco  46925  smfsuplem1  46934  smfsuplem3  46936  smflimsuplem1  46943  smflimsuplem4  46946  smflimsuplem7  46949  cnneiima  49042  seposep  49051  iscnrm3rlem4  49068  iscnrm3llem1  49074  lubsscl  49085  glbsscl  49086  toplatglb  49126  setrecsss  49827  elpglem1  49837