Theorem sstrd 3992

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

Syntax hints:   → wi 4   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  sstrid  3993  sstrdi  3994  rabssrabd  4081  ssdif2d  4143  uniintsn  4991  funss  6565  fssxp  6743  knatar  7351  tfisi  7845  suppssov1  8180  suppssfv  8184  tposss  8209  frrlem8  8275  tfrlem1  8373  omwordri  8569  oewordri  8589  oeeui  8599  oaabs2  8645  omopthlem1  8655  ecinxp  8783  sbthlem1  9080  dffi2  9415  hartogslem1  9534  cantnfcl  9659  cantnflt  9664  cantnfp1lem3  9672  cantnflem3  9683  cnfcom  9692  cnfcom3lem  9695  ttrcltr  9708  rankssb  9840  tskwe  9942  dfac12lem2  10136  dfac12lem3  10137  cfflb  10251  cfcof  10266  ssfin2  10312  hsmexlem4  10421  ttukeylem6  10506  ttukeylem7  10507  fpwwe2lem1  10623  fpwwe2lem7  10629  fpwwe2lem10  10632  fpwwe2lem11  10633  canthnumlem  10640  canthwelem  10642  canthwe  10643  canthp1lem2  10645  pwfseqlem5  10655  wunex2  10730  tsktrss  10753  inttsk  10766  uzwo3  12924  supicc  13475  supiccub  13476  supicclub  13477  ssfzunsnext  13543  seqsplit  13998  seqf1olem2a  14003  seqz  14013  swrdval2  14593  trrelssd  14917  rtrclreclem4  15005  sumss  15667  qshash  15770  incexc  15780  incexc2  15781  prodss  15888  rpnnen2lem11  16164  vdwlem1  16911  ramub1lem1  16956  imasaddvallem  17472  imasvscaf  17482  mrerintcl  17538  ismred2  17544  mremre  17545  mrcuni  17562  mressmrcd  17568  submrc  17569  mrissmrid  17582  mreexexlem2d  17586  isacs2  17594  isacs1i  17598  invss  17705  ssctr  17769  funcres2b  17844  isacs3lem  18492  acsfiindd  18503  acsmapd  18504  acsmap2d  18505  tsrdir  18554  subsubm  18694  gsumwspan  18724  subsubg  19024  subgint  19025  cntzidss  19199  symggen  19333  pmtrdifellem1  19339  pmtrdifellem2  19340  pgpssslw  19477  lsmless1x  19507  lsmless2x  19508  lsmless12  19525  subglsm  19536  gsumval3lem2  19769  gsumzaddlem  19784  gsumzadd  19785  gsum2d  19835  dmdprdd  19864  dprdfeq0  19887  dprdspan  19892  dprdres  19893  dprdss  19894  dprdz  19895  subgdmdprd  19899  subgdprd  19900  dprdsn  19901  dprd2dlem1  19906  dprd2da  19907  dmdprdsplit2lem  19910  dprdsplit  19913  pgpfac1lem2  19940  pgpfac1lem3  19942  pgpfac1lem5  19944  subsubrg  20383  subdrgint  20412  lspss  20588  lspun  20591  lsslsp  20619  lmhmlsp  20653  lsmelval2  20689  lsmssspx  20692  lsppratlem2  20754  lsppratlem3  20755  lsppratlem4  20756  lbsextlem2  20765  lbsextlem3  20766  ocvlsp  21221  cssmre  21238  obselocv  21275  obslbs  21277  aspss  21423  mhpaddcl  21686  mhpinvcl  21687  mhpvscacl  21689  toponmre  22589  neiint  22600  neiss  22605  lpss  22638  lpss3  22640  restopnb  22671  restfpw  22675  neitr  22676  restcls  22677  restntr  22678  restlp  22679  ordtbas  22688  pnfnei  22716  mnfnei  22717  iscnp4  22759  cnclsi  22768  isreg2  22873  discmp  22894  cmpcld  22898  uncmp  22899  sscmp  22901  hauscmplem  22902  cmpfi  22904  iunconnlem  22923  clsconn  22926  2ndcctbss  22951  restnlly  22978  llyrest  22981  nllyrest  22982  llyidm  22984  nllyidm  22985  cldllycmp  22991  dislly  22993  comppfsc  23028  llycmpkgen2  23046  ptbasfi  23077  txnlly  23133  txcmplem1  23137  tx1stc  23146  xkococnlem  23155  qtopval2  23192  basqtop  23207  tgqtop  23208  qtoprest  23213  kqreglem1  23237  kqreglem2  23238  kqnrmlem1  23239  kqnrmlem2  23240  fsubbas  23363  fgabs  23375  fbasrn  23380  trfil2  23383  trfg  23387  isufil2  23404  trufil  23406  ssufl  23414  ufileu  23415  filufint  23416  fmfnfmlem4  23453  fmfnfm  23454  flimss2  23468  flimss1  23469  fclsfnflim  23523  flimfnfcls  23524  fclscmp  23526  cnpfcfi  23536  alexsubALT  23547  clssubg  23605  clsnsg  23606  tsmsres  23640  ustexsym  23712  ustex2sym  23713  ustex3sym  23714  ustneism  23720  trust  23726  utoptop  23731  restutopopn  23735  utop2nei  23747  utopreg  23749  cfiluweak  23792  neipcfilu  23793  blssps  23922  blss  23923  blcld  24006  blsscls  24008  met1stc  24022  met2ndci  24023  metust  24059  cfilucfil  24060  restmetu  24071  tgqioo  24308  xrsblre  24319  reconnlem2  24335  xrge0gsumle  24341  xrge0tsms  24342  rescncf  24405  cnmpopc  24436  cnheibor  24463  cnllycmp  24464  lebnum  24472  phtpycn  24491  cfilfcls  24783  iscmet3lem2  24801  cmetss  24825  cncmet  24831  bcthlem4  24836  bcth3  24840  rrxcph  24901  rrxmetlem  24916  minveclem4a  24939  minveclem4  24941  ivthicc  24967  ovollb  24988  ovollb2lem  24997  ovollb2  24998  nulmbl2  25045  ioorcl2  25081  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  opnmbllem  25110  volcn  25115  volivth  25116  mbfeqalem1  25150  itg10a  25220  mbfi1fseqlem4  25228  ditgcl  25367  ditgswap  25368  ditgsplitlem  25369  limcflf  25390  limcres  25395  dvbss  25410  dvbsss  25411  perfdvf  25412  dvreslem  25418  dvres2lem  25419  dvres3  25422  dvmptresicc  25425  dvcnp  25428  dvcnp2  25429  dvcn  25430  dvnff  25432  dvn2bss  25439  dvnres  25440  cpnord  25444  dvaddbr  25447  dvmulbr  25448  dvcobr  25455  dvnfre  25461  dvmptres2  25471  dvmptntr  25480  dvcnvlem  25485  dvcnv  25486  dvferm1lem  25493  dvferm2lem  25495  dvlip  25502  dvlipcn  25503  dvlip2  25504  c1liplem1  25505  dvgt0lem1  25511  lhop1lem  25522  lhop  25525  dvcnvrelem1  25526  dvcnvrelem2  25527  dvcnvre  25528  dvfsumle  25530  dvfsumge  25531  dvfsumabs  25532  ftc1lem1  25544  ftc1lem2  25545  ftc1a  25546  ftc1lem4  25548  ftc2ditglem  25554  itgsubstlem  25557  ig1peu  25681  ig1pdvds  25686  taylfvallem1  25861  tayl0  25866  taylply2  25872  taylply  25873  dvtaylp  25874  dvntaylp  25875  dvntaylp0  25876  taylthlem1  25877  ulmdvlem1  25904  ulmdvlem3  25906  psercn  25930  pserdvlem2  25932  abelth  25945  xrlimcnp  26463  lgamucov  26532  wilthlem2  26563  sqff1o  26676  chtublem  26704  pntlemq  27094  pntlemf  27098  sssslt1  27286  sssslt2  27287  scutbdaybnd  27306  scutbdaybnd2  27307  cofss  27407  coiniss  27408  tglineintmo  27883  ttgcontlem1  28132  pthdlem1  29013  shintcli  30570  shub1  30623  mdslmd1lem1  31566  mdexchi  31576  chirredlem1  31631  mdsymlem5  31648  sumdmdii  31656  sumdmdlem2  31660  fnpreimac  31884  fsuppinisegfi  31897  xrsupssd  31960  xrge0infssd  31962  swrdrn3  32107  swrdf1  32108  swrdrndisj  32109  pwrssmgc  32158  xrge0tsmsd  32197  fldgenss  32395  fldgenssp  32397  linds2eq  32486  elrspunidl  32535  mxidlprm  32575  ssmxidllem  32578  ssmxidl  32579  qsdrnglem2  32599  lbsdiflsp0  32700  dimkerim  32701  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  smatrcl  32765  locfinreflem  32809  cmpcref  32819  zarclsun  32839  zarclsiin  32840  zarclssn  32842  zarcmplem  32850  pnfneige0  32920  esum2d  33080  insiga  33124  sssigagen2  33133  dynkin  33154  dya2iocnei  33270  omsmon  33286  carsgclctunlem1  33305  carsggect  33306  omsmeas  33311  ftc2re  33599  fdvneggt  33601  fdvnegge  33603  reprsuc  33616  reprss  33618  reprlt  33620  reprinfz1  33623  logdivsqrle  33651  hgt750lemb  33657  bnj906  33930  bnj1020  33965  bnj1137  33995  bnj1408  34036  bnj1452  34052  erdszelem7  34177  erdszelem8  34178  erdsze2lem1  34183  connpconn  34215  cvmliftmolem1  34261  cvmlift2lem1  34282  cvmlift2lem9  34291  cvmlift2lem10  34292  cvmlift3lem6  34304  cvmlift3lem7  34305  satfsschain  34344  ss2mcls  34548  gg-dvcnp2  35163  gg-dvmulbr  35164  gg-dvcobr  35165  gg-dvfsumle  35171  neibastop2lem  35234  fnemeet2  35241  fnejoin1  35242  ontgval  35305  unbdqndv1  35373  opnmbllem0  36513  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  sstotbnd2  36631  heiborlem1  36668  heiborlem8  36675  intidl  36886  lsmsat  37867  lssats  37871  lpssat  37872  lssatle  37874  lssat  37875  lsatcvatlem  37908  paddss12  38679  paddasslem17  38696  pmodlem1  38706  pmod1i  38708  pmodl42N  38711  elpcliN  38753  pclfinN  38760  polcon3N  38777  polcon2N  38779  paddunN  38787  pclfinclN  38810  poml5N  38814  osumcllem1N  38816  osumcllem2N  38817  osumcllem3N  38818  pl42lem2N  38840  pl42lem4N  38842  cdlemn5pre  40060  dihord1  40078  dihord2a  40079  dihord2b  40080  dihord5b  40119  dochss  40225  dochdmj1  40250  djhsumss  40267  djhunssN  40269  dochexmidlem2  40321  lclkrslem1  40397  lclkrslem2  40398  lcfrlem2  40403  aks4d1p4  40933  aks4d1p5  40934  aks4d1p7  40937  aks4d1p8  40941  sticksstones1  40951  prjcrv0  41372  elrfi  41418  ismrcd1  41422  istopclsd  41424  mrefg2  41431  aomclem2  41783  aomclem6  41787  hbtlem6  41857  hbt  41858  oege2  42043  cantnftermord  42056  omabs2  42068  tfsconcat0b  42082  naddgeoa  42131  naddwordnexlem0  42133  naddwordnexlem1  42134  dfno2  42165  mptrcllem  42350  dfrcl2  42411  relexp0a  42453  trclimalb2  42463  frege81d  42484  k0004ss2  42889  imo72b2lem0  42903  imo72b2lem2  42905  imo72b2  42910  uzwo4  43726  ssin0  43728  ixpssmapc  43747  ssinc  43762  ssdec  43763  supxrre3  44022  uzfissfz  44023  ssuzfz  44046  supminfxr  44161  inficc  44234  ressiocsup  44254  ressioosup  44255  ressiooinf  44257  limccog  44323  limclner  44354  limsupres  44408  limsupresuz2  44412  limsupequzlem  44425  limsupvaluz2  44441  supcnvlimsup  44443  limsupgtlem  44480  liminfresuz2  44490  cncfmptssg  44574  cncfuni  44589  icccncfext  44590  dvresntr  44621  dvbdfbdioolem1  44631  dvdmsscn  44639  dvnxpaek  44645  dvnprodlem2  44650  stoweidlem59  44762  fourierdlem20  44830  fourierdlem42  44852  fourierdlem48  44857  fourierdlem49  44858  fourierdlem52  44861  fourierdlem58  44867  fourierdlem64  44873  fourierdlem73  44882  fourierdlem76  44885  fourierdlem80  44889  fourierdlem84  44893  fourierdlem93  44902  fourierdlem103  44912  fourierdlem104  44913  fourierdlem113  44922  etransclem18  44955  ioorrnopnlem  45007  salincl  45027  intsal  45033  fsumlesge0  45080  sge0cl  45084  sge0supre  45092  sge0less  45095  sge0split  45112  sge0seq  45149  caragensspw  45212  omessre  45213  caragendifcl  45217  caratheodorylem1  45229  0ome  45232  omess0  45237  caragencmpl  45238  hoicvr  45251  hoissrrn  45252  hoicvrrex  45259  ovnlecvr  45261  ovnsslelem  45263  ovnssle  45264  ovnsubaddlem1  45273  hoissrrn2  45281  hoidmv1lelem1  45294  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem4  45301  ovnlecvr2  45313  voncmpl  45324  hspmbl  45332  opnvonmbllem1  45335  ovolval5lem2  45356  ovolval5lem3  45357  vonioolem1  45383  pimdecfgtioc  45418  pimincfltioc  45419  pimdecfgtioo  45420  pimincfltioo  45421  issmflem  45430  cnfsmf  45443  incsmflem  45444  smfsssmf  45446  smfadd  45468  decsmflem  45469  smflim  45480  smfres  45493  smfmul  45498  smfpimbor1lem1  45501  smfco  45505  smfsuplem1  45514  smfsuplem3  45516  smflimsuplem1  45523  smflimsuplem4  45526  smflimsuplem7  45529  subsubmgm  46554  subsubrng  46727  cnneiima  47503  seposep  47512  iscnrm3rlem4  47530  iscnrm3llem1  47536  lubsscl  47547  glbsscl  47548  toplatglb  47580  setrecsss  47700  elpglem1  47710