Theorem sstrd 3918

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3896

This theorem is used by:  sstrid  3919  sstrdi  3920  rabssrabd  4008  ssdif2d  4084  uniintsn  4944  funss  6558  fssxp  6737  knatar  7367  tfisi  7870  suppssov1  8217  suppssov2  8218  suppssfv  8222  tposss  8247  frrlem8  8314  tfrlem1  8386  omwordri  8583  oewordri  8604  oeeui  8614  oaabs2  8661  omopthlem1  8671  ecinxp  8816  sbthlem1  9109  dffi2  9418  hartogslem1  9539  cantnfcl  9671  cantnflt  9676  cantnfp1lem3  9684  cantnflem3  9695  cnfcom  9704  cnfcom3lem  9707  ttrcltr  9720  rankssb  9865  rankval4b  9883  tskwe  10034  dfac12lem2  10226  dfac12lem3  10227  cfflb  10340  cfcof  10355  ssfin2  10401  hsmexlem4  10510  ttukeylem6  10595  ttukeylem7  10596  fpwwe2lem1  10719  fpwwe2lem7  10725  fpwwe2lem10  10728  fpwwe2lem11  10729  canthnumlem  10736  canthwelem  10738  canthwe  10739  canthp1lem2  10741  pwfseqlem5  10751  wunex2  10826  tsktrss  10849  inttsk  10862  uzwo3  13073  xrsupssd  13466  supicc  13635  supiccub  13636  supicclub  13637  ssfzunsnext  13706  seqsplit  14181  seqf1olem2a  14186  seqz  14196  swrdval2  14798  swrdf1  14803  swrdrn3  14806  trrelssd  15131  rtrclreclem4  15219  sumss  15895  qshash  15999  incexc  16011  incexc2  16012  prodss  16119  rpnnen2lem11  16397  vdwlem1  17164  ramub1lem1  17209  imasaddvallem  17706  imasvscaf  17716  mrerintcl  17772  ismred2  17778  mremre  17779  mrcuni  17800  mressmrcd  17806  submrc  17807  mrissmrid  17820  mreexexlem2d  17824  isacs2  17832  isacs1i  17836  invss  17941  ssctr  18005  funcres2b  18077  isacs3lem  18721  acsfiindd  18732  acsmapd  18733  acsmap2d  18734  tsrdir  18783  subsubmgm  18904  subsubm  19017  gsumwspan  19047  subsubg  19365  subgint  19366  cntzidss  19559  symggen  19689  pmtrdifellem1  19695  pmtrdifellem2  19696  pgpssslw  19833  lsmless1x  19863  lsmless2x  19864  lsmless12  19881  subglsm  19892  gsumval3lem2  20125  gsumzaddlem  20140  gsumzadd  20141  gsum2d  20191  dmdprdd  20220  dprdfeq0  20243  dprdspan  20248  dprdres  20249  dprdss  20250  dprdz  20251  subgdmdprd  20255  subgdprd  20256  dprdsn  20257  dprd2dlem1  20262  dprd2da  20263  dmdprdsplit2lem  20266  dprdsplit  20269  pgpfac1lem2  20296  pgpfac1lem3  20298  pgpfac1lem5  20300  subsubrng  20820  subsubrg  20855  subdrgint  21065  lspss  21264  lspun  21267  lsslsp  21295  lmhmlsp  21329  lsmelval2  21365  lsmssspx  21368  lsppratlem2  21431  lsppratlem3  21432  lsppratlem4  21433  lbsextlem2  21442  lbsextlem3  21443  ssdifidllem  21645  ssdifidlprm  21647  ocvlsp  21987  cssmre  22004  obselocv  22039  obslbs  22041  aspss  22189  mhpaddcl  22477  mhpinvcl  22478  mhpvscacl  22480  psdmullem  22491  toponmre  23416  neiint  23427  neiss  23432  lpss  23465  lpss3  23467  restopnb  23498  restfpw  23502  neitr  23503  restcls  23504  restntr  23505  restlp  23506  ordtbas  23515  pnfnei  23543  mnfnei  23544  iscnp4  23586  cnclsi  23595  isreg2  23700  discmp  23721  cmpcld  23725  uncmp  23726  sscmp  23728  hauscmplem  23729  cmpfi  23731  iunconnlem  23750  clsconn  23753  2ndcctbss  23779  restnlly  23806  llyrest  23809  nllyrest  23810  llyidm  23812  nllyidm  23813  cldllycmp  23819  dislly  23821  comppfsc  23856  llycmpkgen2  23874  ptbasfi  23905  txnlly  23961  txcmplem1  23965  tx1stc  23974  xkococnlem  23983  qtopval2  24020  basqtop  24035  tgqtop  24036  qtoprest  24041  kqreglem1  24065  kqreglem2  24066  kqnrmlem1  24067  kqnrmlem2  24068  fsubbas  24191  fgabs  24203  fbasrn  24208  trfil2  24211  trfg  24215  isufil2  24232  trufil  24234  ssufl  24242  ufileu  24243  filufint  24244  fmfnfmlem4  24281  fmfnfm  24282  flimss2  24296  flimss1  24297  fclsfnflim  24351  flimfnfcls  24352  fclscmp  24354  cnpfcfi  24364  alexsubALT  24375  clssubg  24433  clsnsg  24434  tsmsres  24468  ustexsym  24540  ustex2sym  24541  ustex3sym  24542  ustneism  24548  trust  24553  utoptop  24558  restutopopn  24562  utop2nei  24574  utopreg  24576  cfiluweak  24618  neipcfilu  24619  blssps  24748  blss  24749  blcld  24829  blsscls  24831  met1stc  24845  met2ndci  24846  metust  24882  cfilucfil  24883  restmetu  24894  tgqioo  25124  xrsblre  25136  reconnlem2  25152  xrge0gsumle  25158  xrge0tsms  25159  rescncf  25223  cnmpopc  25254  cnheibor  25281  cnllycmp  25282  lebnum  25290  phtpycn  25309  cfilfcls  25600  iscmet3lem2  25618  cmetss  25642  cncmet  25648  bcthlem4  25653  bcth3  25657  rrxcph  25718  rrxmetlem  25733  minveclem4a  25756  minveclem4  25758  ivthicc  25784  ovollb  25805  ovollb2lem  25814  ovollb2  25815  nulmbl2  25862  ioorcl2  25898  uniioombllem3  25911  uniioombllem4  25912  uniioombllem5  25913  opnmbllem  25927  volcn  25932  volivth  25933  mbfeqalem1  25967  itg10a  26036  mbfi1fseqlem4  26044  ditgcl  26183  ditgswap  26184  ditgsplitlem  26185  limcflf  26206  limcres  26211  dvbss  26226  dvbsss  26227  perfdvf  26228  dvreslem  26234  dvres2lem  26235  dvres3  26238  dvmptresicc  26241  dvcnp  26244  dvcnp2  26245  dvcn  26246  dvnff  26248  dvn2bss  26255  dvnres  26256  cpnord  26260  dvaddbr  26263  dvmulbr  26264  dvcobr  26271  dvnfre  26277  dvmptres2  26287  dvmptntr  26296  dvcnvlem  26301  dvcnv  26302  dvferm1lem  26309  dvferm2lem  26311  dvlip  26318  dvlipcn  26319  dvlip2  26320  c1liplem1  26321  dvgt0lem1  26327  lhop1lem  26338  lhop  26341  dvcnvrelem1  26342  dvcnvrelem2  26343  dvcnvre  26344  dvfsumle  26346  dvfsumge  26347  dvfsumabs  26348  ftc1lem1  26360  ftc1lem2  26361  ftc1a  26362  ftc1lem4  26364  ftc2ditglem  26370  itgsubstlem  26373  ig1peu  26498  ig1pdvds  26503  taylfvallem1  26689  tayl0  26694  taylply2  26700  taylply  26701  dvtaylp  26702  dvntaylp  26703  dvntaylp0  26704  taylthlem1  26705  ulmdvlem1  26732  ulmdvlem3  26734  psercn  26758  pserdvlem2  26760  abelth  26773  xrlimcnp  27301  lgamucov  27370  wilthlem2  27401  sqff1o  27514  chtublem  27543  pntlemq  27933  pntlemf  27937  ssslts1  28164  ssslts2  28165  cutbdaybnd  28186  cutbdaybnd2  28187  eqcuts3  28195  cofss  28321  coiniss  28322  bdaypw2bnd  28856  bdayfinbndlem1  28858  z12bdaylem2  28862  tglineintmo  29115  ttgcontlem1  29467  pthdlem1  30357  shintcli  31936  shub1  31989  mdslmd1lem1  32932  mdexchi  32942  chirredlem1  32997  mdsymlem5  33014  sumdmdii  33022  sumdmdlem2  33026  fnpreimac  33311  fsuppinisegfi  33327  xrge0infssd  33399  swrdrndisj  33564  pwrssmgc  33607  xrge0tsmsd  33680  elrgspnlem4  33852  elrgspnsubrunlem1  33854  elrgspnsubrunlem2  33855  fldgenss  33924  fldgenssp  33926  linds2eq  33982  elrspunidl  34024  mxidlprm  34041  ssmxidllem  34044  ssmxidl  34045  qsdrnglem2  34066  rprmdvdsprod  34112  ressply1evls1  34143  resssra  34265  lsssra  34266  exsslsb  34275  lbsdiflsp0  34304  dimkerim  34305  fedgmullem1  34307  fedgmullem2  34308  fedgmul  34309  dimlssid  34310  fldextrspunlsplem  34351  fldextrspunlsp  34352  fldextrspunlem1  34353  fldextrspundgdvdslem  34358  fldextrspundgdvds  34359  constr01  34420  constrmon  34422  constrextdg2lem  34426  constrfiss  34429  smatrcl  34474  locfinreflem  34518  cmpcref  34528  zarclsun  34548  zarclsiin  34549  zarclssn  34551  zarcmplem  34559  pnfneige0  34629  esum2d  34771  insiga  34816  sssigagen2  34825  dynkin  34846  dya2iocnei  34960  omsmon  34976  carsgclctunlem1  34995  carsggect  34996  omsmeas  35001  ftc2re  35273  fdvneggt  35275  fdvnegge  35277  reprsuc  35290  reprss  35292  reprlt  35294  reprinfz1  35297  logdivsqrle  35325  hgt750lemb  35331  bnj906  35606  bnj1020  35641  bnj1137  35671  bnj1408  35712  bnj1452  35728  abweex  35769  fineqvnttrclselem2  35846  erdszelem7  36048  erdszelem8  36049  erdsze2lem1  36054  connpconn  36086  cvmliftmolem1  36132  cvmlift2lem1  36153  cvmlift2lem9  36162  cvmlift2lem10  36163  cvmlift3lem6  36175  cvmlift3lem7  36176  satfsschain  36215  ss2mcls  36419  neibastop2lem  37240  fnemeet2  37247  fnejoin1  37248  ontgval  37311  ttcmin  37376  unbdqndv1  37466  opnmbllem0  38667  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  sstotbnd2  38801  heiborlem1  38838  heiborlem8  38845  intidl  39056  lsmsat  40158  lssats  40162  lpssat  40163  lssatle  40165  lssat  40166  lsatcvatlem  40199  paddss12  40969  paddasslem17  40986  pmodlem1  40996  pmod1i  40998  pmodl42N  41001  elpcliN  41043  pclfinN  41050  polcon3N  41067  polcon2N  41069  paddunN  41077  pclfinclN  41100  poml5N  41104  osumcllem1N  41106  osumcllem2N  41107  osumcllem3N  41108  pl42lem2N  41130  pl42lem4N  41132  cdlemn5pre  42350  dihord1  42368  dihord2a  42369  dihord2b  42370  dihord5b  42409  dochss  42515  dochdmj1  42540  djhsumss  42557  djhunssN  42559  dochexmidlem2  42611  lclkrslem1  42687  lclkrslem2  42688  lcfrlem2  42693  aks4d1p4  43222  aks4d1p5  43223  aks4d1p7  43226  aks4d1p8  43230  aks6d1c2  43273  sticksstones1  43289  unitscyglem5  43342  prjcrv0  43762  elrfi  43798  ismrcd1  43802  istopclsd  43804  mrefg2  43811  aomclem2  44150  aomclem6  44154  hbtlem6  44224  hbt  44225  oege2  44402  cantnftermord  44415  omabs2  44427  tfsconcat0b  44441  naddgeoa  44489  naddwordnexlem0  44491  naddwordnexlem1  44492  dfno2  44522  mptrcllem  44706  dfrcl2  44767  relexp0a  44809  trclimalb2  44819  frege81d  44840  k0004ss2  45245  imo72b2lem2  45260  imo72b2  45265  dmstructnn  46019  ishfstruct  46121  uzwo4  46163  ssin0  46165  ixpssmapc  46183  ssinc  46195  ssdec  46196  supxrre3  46430  uzfissfz  46431  ssuzfz  46454  supminfxr  46567  inficc  46639  ressiocsup  46659  ressioosup  46660  ressiooinf  46662  limccog  46725  limclner  46754  limsupres  46808  limsupresuz2  46812  limsupequzlem  46825  supcnvlimsup  46843  limsupgtlem  46880  liminfresuz2  46890  cncfmptssg  46974  icccncfext  46990  dvresntr  47021  dvbdfbdioolem1  47031  dvdmsscn  47039  dvnxpaek  47045  dvnprodlem2  47050  stoweidlem59  47162  fourierdlem20  47230  fourierdlem42  47252  fourierdlem48  47257  fourierdlem49  47258  fourierdlem52  47261  fourierdlem58  47267  fourierdlem64  47273  fourierdlem73  47282  fourierdlem76  47285  fourierdlem80  47289  fourierdlem84  47293  fourierdlem93  47302  fourierdlem103  47312  fourierdlem104  47313  fourierdlem113  47322  etransclem18  47355  ioorrnopnlem  47407  salincl  47427  intsal  47433  fsumlesge0  47480  sge0cl  47484  sge0supre  47492  sge0less  47495  sge0split  47512  sge0seq  47549  caragensspw  47612  omessre  47613  caragendifcl  47617  caratheodorylem1  47629  0ome  47632  omess0  47637  caragencmpl  47638  hoissrrn  47652  hoicvrrex  47659  ovnlecvr  47661  ovnsslelem  47663  ovnssle  47664  ovnsubaddlem1  47673  hoissrrn2  47681  hoidmv1lelem1  47694  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem4  47701  ovnlecvr2  47713  voncmpl  47724  hspmbl  47732  opnvonmbllem1  47735  ovolval5lem2  47756  ovolval5lem3  47757  vonioolem1  47783  pimdecfgtioc  47818  pimincfltioc  47819  pimdecfgtioo  47820  pimincfltioo  47821  issmflem  47830  cnfsmf  47843  incsmflem  47844  smfsssmf  47846  smfadd  47868  decsmflem  47869  smflim  47880  smfres  47893  smfmul  47898  smfpimbor1lem1  47901  smfco  47905  smfsuplem1  47914  smfsuplem3  47916  smflimsuplem1  47923  smflimsuplem4  47926  smflimsuplem7  47929  tmachlem-agreeprod  48040  nndivides2  48547  cnneiima  50124  seposep  50133  iscnrm3rlem4  50150  iscnrm3llem1  50156  lubsscl  50167  glbsscl  50168  toplatglb  50208  setrecsss  50962  elpglem1  50972