Theorem sstrd 3945

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

Syntax hints:   → wi 4   ⊆ wss 3902

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 3919

This theorem is referenced by:  sstrid  3946  sstrdi  3947  rabssrabd  4033  ssdif2d  4098  uniintsn  4935  funss  6500  fssxp  6678  knatar  7291  tfisi  7789  suppssov1  8127  suppssov2  8128  suppssfv  8132  tposss  8157  frrlem8  8223  tfrlem1  8295  omwordri  8487  oewordri  8507  oeeui  8517  oaabs2  8564  omopthlem1  8574  ecinxp  8716  sbthlem1  9000  dffi2  9307  hartogslem1  9428  cantnfcl  9557  cantnflt  9562  cantnfp1lem3  9570  cantnflem3  9581  cnfcom  9590  cnfcom3lem  9593  ttrcltr  9606  rankssb  9741  tskwe  9843  dfac12lem2  10036  dfac12lem3  10037  cfflb  10150  cfcof  10165  ssfin2  10211  hsmexlem4  10320  ttukeylem6  10405  ttukeylem7  10406  fpwwe2lem1  10522  fpwwe2lem7  10528  fpwwe2lem10  10531  fpwwe2lem11  10532  canthnumlem  10539  canthwelem  10541  canthwe  10542  canthp1lem2  10544  pwfseqlem5  10554  wunex2  10629  tsktrss  10652  inttsk  10665  uzwo3  12841  xrsupssd  13232  supicc  13401  supiccub  13402  supicclub  13403  ssfzunsnext  13469  seqsplit  13942  seqf1olem2a  13947  seqz  13957  swrdval2  14554  trrelssd  14880  rtrclreclem4  14968  sumss  15631  qshash  15734  incexc  15744  incexc2  15745  prodss  15854  rpnnen2lem11  16133  vdwlem1  16893  ramub1lem1  16938  imasaddvallem  17433  imasvscaf  17443  mrerintcl  17499  ismred2  17505  mremre  17506  mrcuni  17527  mressmrcd  17533  submrc  17534  mrissmrid  17547  mreexexlem2d  17551  isacs2  17559  isacs1i  17563  invss  17668  ssctr  17732  funcres2b  17804  isacs3lem  18448  acsfiindd  18459  acsmapd  18460  acsmap2d  18461  tsrdir  18510  subsubmgm  18618  subsubm  18724  gsumwspan  18754  subsubg  19062  subgint  19063  cntzidss  19253  symggen  19383  pmtrdifellem1  19389  pmtrdifellem2  19390  pgpssslw  19527  lsmless1x  19557  lsmless2x  19558  lsmless12  19575  subglsm  19586  gsumval3lem2  19819  gsumzaddlem  19834  gsumzadd  19835  gsum2d  19885  dmdprdd  19914  dprdfeq0  19937  dprdspan  19942  dprdres  19943  dprdss  19944  dprdz  19945  subgdmdprd  19949  subgdprd  19950  dprdsn  19951  dprd2dlem1  19956  dprd2da  19957  dmdprdsplit2lem  19960  dprdsplit  19963  pgpfac1lem2  19990  pgpfac1lem3  19992  pgpfac1lem5  19994  subsubrng  20479  subsubrg  20514  subdrgint  20719  lspss  20918  lspun  20921  lsslsp  20949  lsslspOLD  20950  lmhmlsp  20984  lsmelval2  21020  lsmssspx  21023  lsppratlem2  21086  lsppratlem3  21087  lsppratlem4  21088  lbsextlem2  21097  lbsextlem3  21098  ocvlsp  21614  cssmre  21631  obselocv  21666  obslbs  21668  aspss  21815  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  29745  shintcli  31307  shub1  31360  mdslmd1lem1  32303  mdexchi  32313  chirredlem1  32368  mdsymlem5  32385  sumdmdii  32393  sumdmdlem2  32397  fnpreimac  32651  fsuppinisegfi  32666  xrge0infssd  32742  swrdrn3  32934  swrdf1  32935  swrdrndisj  32936  pwrssmgc  32979  xrge0tsmsd  33040  elrgspnlem4  33210  elrgspnsubrunlem1  33212  elrgspnsubrunlem2  33213  fldgenss  33280  fldgenssp  33282  linds2eq  33344  elrspunidl  33391  ssdifidllem  33419  ssdifidlprm  33421  mxidlprm  33433  ssmxidllem  33436  ssmxidl  33437  qsdrnglem2  33459  rprmdvdsprod  33497  ressply1evls1  33526  resssra  33597  lsssra  33598  exsslsb  33607  lbsdiflsp0  33637  dimkerim  33638  fedgmullem1  33640  fedgmullem2  33641  fedgmul  33642  dimlssid  33643  fldextrspunlsplem  33684  fldextrspunlsp  33685  fldextrspunlem1  33686  fldextrspundgdvdslem  33691  fldextrspundgdvds  33692  constr01  33753  constrmon  33755  constrextdg2lem  33759  constrfiss  33762  smatrcl  33807  locfinreflem  33851  cmpcref  33861  zarclsun  33881  zarclsiin  33882  zarclssn  33884  zarcmplem  33892  pnfneige0  33962  esum2d  34104  insiga  34148  sssigagen2  34157  dynkin  34178  dya2iocnei  34293  omsmon  34309  carsgclctunlem1  34328  carsggect  34329  omsmeas  34334  ftc2re  34609  fdvneggt  34611  fdvnegge  34613  reprsuc  34626  reprss  34628  reprlt  34630  reprinfz1  34633  logdivsqrle  34661  hgt750lemb  34667  bnj906  34940  bnj1020  34975  bnj1137  35005  bnj1408  35046  bnj1452  35062  rankval4b  35109  fineqvnttrclselem2  35140  erdszelem7  35239  erdszelem8  35240  erdsze2lem1  35245  connpconn  35277  cvmliftmolem1  35323  cvmlift2lem1  35344  cvmlift2lem9  35353  cvmlift2lem10  35354  cvmlift3lem6  35366  cvmlift3lem7  35367  satfsschain  35406  ss2mcls  35610  neibastop2lem  36400  fnemeet2  36407  fnejoin1  36408  ontgval  36471  unbdqndv1  36548  opnmbllem0  37702  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  sstotbnd2  37820  heiborlem1  37857  heiborlem8  37864  intidl  38075  lsmsat  39053  lssats  39057  lpssat  39058  lssatle  39060  lssat  39061  lsatcvatlem  39094  paddss12  39864  paddasslem17  39881  pmodlem1  39891  pmod1i  39893  pmodl42N  39896  elpcliN  39938  pclfinN  39945  polcon3N  39962  polcon2N  39964  paddunN  39972  pclfinclN  39995  poml5N  39999  osumcllem1N  40001  osumcllem2N  40002  osumcllem3N  40003  pl42lem2N  40025  pl42lem4N  40027  cdlemn5pre  41245  dihord1  41263  dihord2a  41264  dihord2b  41265  dihord5b  41304  dochss  41410  dochdmj1  41435  djhsumss  41452  djhunssN  41454  dochexmidlem2  41506  lclkrslem1  41582  lclkrslem2  41583  lcfrlem2  41588  aks4d1p4  42118  aks4d1p5  42119  aks4d1p7  42122  aks4d1p8  42126  aks6d1c2  42169  sticksstones1  42185  unitscyglem5  42238  prjcrv0  42672  elrfi  42733  ismrcd1  42737  istopclsd  42739  mrefg2  42746  aomclem2  43094  aomclem6  43098  hbtlem6  43168  hbt  43169  oege2  43346  cantnftermord  43359  omabs2  43371  tfsconcat0b  43385  naddgeoa  43433  naddwordnexlem0  43435  naddwordnexlem1  43436  dfno2  43467  mptrcllem  43652  dfrcl2  43713  relexp0a  43755  trclimalb2  43765  frege81d  43786  k0004ss2  44191  imo72b2lem2  44206  imo72b2  44211  uzwo4  45096  ssin0  45098  ixpssmapc  45116  ssinc  45130  ssdec  45131  supxrre3  45370  uzfissfz  45371  ssuzfz  45394  supminfxr  45508  inficc  45580  ressiocsup  45600  ressioosup  45601  ressiooinf  45603  limccog  45666  limclner  45695  limsupres  45749  limsupresuz2  45753  limsupequzlem  45766  supcnvlimsup  45784  limsupgtlem  45821  liminfresuz2  45831  cncfmptssg  45915  cncfuni  45930  icccncfext  45931  dvresntr  45962  dvbdfbdioolem1  45972  dvdmsscn  45980  dvnxpaek  45986  dvnprodlem2  45991  stoweidlem59  46103  fourierdlem20  46171  fourierdlem42  46193  fourierdlem48  46198  fourierdlem49  46199  fourierdlem52  46202  fourierdlem58  46208  fourierdlem64  46214  fourierdlem73  46223  fourierdlem76  46226  fourierdlem80  46230  fourierdlem84  46234  fourierdlem93  46243  fourierdlem103  46253  fourierdlem104  46254  fourierdlem113  46263  etransclem18  46296  ioorrnopnlem  46348  salincl  46368  intsal  46374  fsumlesge0  46421  sge0cl  46425  sge0supre  46433  sge0less  46436  sge0split  46453  sge0seq  46490  caragensspw  46553  omessre  46554  caragendifcl  46558  caratheodorylem1  46570  0ome  46573  omess0  46578  caragencmpl  46579  hoicvr  46592  hoissrrn  46593  hoicvrrex  46600  ovnlecvr  46602  ovnsslelem  46604  ovnssle  46605  ovnsubaddlem1  46614  hoissrrn2  46622  hoidmv1lelem1  46635  hoidmvlelem1  46639  hoidmvlelem2  46640  hoidmvlelem4  46642  ovnlecvr2  46654  voncmpl  46665  hspmbl  46673  opnvonmbllem1  46676  ovolval5lem2  46697  ovolval5lem3  46698  vonioolem1  46724  pimdecfgtioc  46759  pimincfltioc  46760  pimdecfgtioo  46761  pimincfltioo  46762  issmflem  46771  cnfsmf  46784  incsmflem  46785  smfsssmf  46787  smfadd  46809  decsmflem  46810  smflim  46821  smfres  46834  smfmul  46839  smfpimbor1lem1  46842  smfco  46846  smfsuplem1  46855  smfsuplem3  46857  smflimsuplem1  46864  smflimsuplem4  46867  smflimsuplem7  46870  cnneiima  48954  seposep  48963  iscnrm3rlem4  48980  iscnrm3llem1  48986  lubsscl  48997  glbsscl  48998  toplatglb  49038  setrecsss  49739  elpglem1  49749