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 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3904  df-ss 3914

This theorem is referenced by:  sstrid  3942  sstrdi  3943  rabssrabd  4027  ssdif2d  4089  uniintsn  4931  funss  6490  fssxp  6666  knatar  7268  tfisi  7752  suppssov1  8063  suppssfv  8067  tposss  8092  frrlem8  8158  tfrlem1  8256  omwordri  8453  oewordri  8473  oeeui  8483  oaabs2  8529  omopthlem1  8539  ecinxp  8631  sbthlem1  8927  dffi2  9259  hartogslem1  9378  cantnfcl  9503  cantnflt  9508  cantnfp1lem3  9516  cantnflem3  9527  cnfcom  9536  cnfcom3lem  9539  ttrcltr  9552  rankssb  9684  tskwe  9786  dfac12lem2  9980  dfac12lem3  9981  cfflb  10095  cfcof  10110  ssfin2  10156  hsmexlem4  10265  ttukeylem6  10350  ttukeylem7  10351  fpwwe2lem1  10467  fpwwe2lem7  10473  fpwwe2lem10  10476  fpwwe2lem11  10477  canthnumlem  10484  canthwelem  10486  canthwe  10487  canthp1lem2  10489  pwfseqlem5  10499  wunex2  10574  tsktrss  10597  inttsk  10610  uzwo3  12763  supicc  13313  supiccub  13314  supicclub  13315  ssfzunsnext  13381  seqsplit  13836  seqf1olem2a  13841  seqz  13851  swrdval2  14438  trrelssd  14763  rtrclreclem4  14851  sumss  15515  qshash  15618  incexc  15628  incexc2  15629  prodss  15736  rpnnen2lem11  16012  vdwlem1  16759  ramub1lem1  16804  imasaddvallem  17317  imasvscaf  17327  mrerintcl  17383  ismred2  17389  mremre  17390  mrcuni  17407  mressmrcd  17413  submrc  17414  mrissmrid  17427  mreexexlem2d  17431  isacs2  17439  isacs1i  17443  invss  17550  ssctr  17614  funcres2b  17689  isacs3lem  18337  acsfiindd  18348  acsmapd  18349  acsmap2d  18350  tsrdir  18399  subsubm  18532  gsumwspan  18561  subsubg  18854  subgint  18855  cntzidss  19020  symggen  19154  pmtrdifellem1  19160  pmtrdifellem2  19161  pgpssslw  19295  lsmless1x  19325  lsmless2x  19326  lsmless12  19343  subglsm  19354  gsumval3lem2  19582  gsumzaddlem  19597  gsumzadd  19598  gsum2d  19648  dmdprdd  19677  dprdfeq0  19700  dprdspan  19705  dprdres  19706  dprdss  19707  dprdz  19708  subgdmdprd  19712  subgdprd  19713  dprdsn  19714  dprd2dlem1  19719  dprd2da  19720  dmdprdsplit2lem  19723  dprdsplit  19726  pgpfac1lem2  19753  pgpfac1lem3  19755  pgpfac1lem5  19757  subsubrg  20132  subdrgint  20154  lspss  20329  lspun  20332  lsslsp  20360  lmhmlsp  20394  lsmelval2  20430  lsmssspx  20433  lsppratlem2  20493  lsppratlem3  20494  lsppratlem4  20495  lbsextlem2  20504  lbsextlem3  20505  ocvlsp  20964  cssmre  20981  obselocv  21018  obslbs  21020  aspss  21164  mhpaddcl  21424  mhpinvcl  21425  mhpvscacl  21427  toponmre  22327  neiint  22338  neiss  22343  lpss  22376  lpss3  22378  restopnb  22409  restfpw  22413  neitr  22414  restcls  22415  restntr  22416  restlp  22417  ordtbas  22426  pnfnei  22454  mnfnei  22455  iscnp4  22497  cnclsi  22506  isreg2  22611  discmp  22632  cmpcld  22636  uncmp  22637  sscmp  22639  hauscmplem  22640  cmpfi  22642  iunconnlem  22661  clsconn  22664  2ndcctbss  22689  restnlly  22716  llyrest  22719  nllyrest  22720  llyidm  22722  nllyidm  22723  cldllycmp  22729  dislly  22731  comppfsc  22766  llycmpkgen2  22784  ptbasfi  22815  txnlly  22871  txcmplem1  22875  tx1stc  22884  xkococnlem  22893  qtopval2  22930  basqtop  22945  tgqtop  22946  qtoprest  22951  kqreglem1  22975  kqreglem2  22976  kqnrmlem1  22977  kqnrmlem2  22978  fsubbas  23101  fgabs  23113  fbasrn  23118  trfil2  23121  trfg  23125  isufil2  23142  trufil  23144  ssufl  23152  ufileu  23153  filufint  23154  fmfnfmlem4  23191  fmfnfm  23192  flimss2  23206  flimss1  23207  fclsfnflim  23261  flimfnfcls  23262  fclscmp  23264  cnpfcfi  23274  alexsubALT  23285  clssubg  23343  clsnsg  23344  tsmsres  23378  ustexsym  23450  ustex2sym  23451  ustex3sym  23452  ustneism  23458  trust  23464  utoptop  23469  restutopopn  23473  utop2nei  23485  utopreg  23487  cfiluweak  23530  neipcfilu  23531  blssps  23660  blss  23661  blcld  23744  blsscls  23746  met1stc  23760  met2ndci  23761  metust  23797  cfilucfil  23798  restmetu  23809  tgqioo  24046  xrsblre  24057  reconnlem2  24073  xrge0gsumle  24079  xrge0tsms  24080  rescncf  24143  cnmpopc  24174  cnheibor  24201  cnllycmp  24202  lebnum  24210  phtpycn  24229  cfilfcls  24521  iscmet3lem2  24539  cmetss  24563  cncmet  24569  bcthlem4  24574  bcth3  24578  rrxcph  24639  rrxmetlem  24654  minveclem4a  24677  minveclem4  24679  ivthicc  24705  ovollb  24726  ovollb2lem  24735  ovollb2  24736  nulmbl2  24783  ioorcl2  24819  uniioombllem3  24832  uniioombllem4  24833  uniioombllem5  24834  opnmbllem  24848  volcn  24853  volivth  24854  mbfeqalem1  24888  itg10a  24958  mbfi1fseqlem4  24966  ditgcl  25105  ditgswap  25106  ditgsplitlem  25107  limcflf  25128  limcres  25133  dvbss  25148  dvbsss  25149  perfdvf  25150  dvreslem  25156  dvres2lem  25157  dvres3  25160  dvmptresicc  25163  dvcnp  25166  dvcnp2  25167  dvcn  25168  dvnff  25170  dvn2bss  25177  dvnres  25178  cpnord  25182  dvaddbr  25185  dvmulbr  25186  dvcobr  25193  dvnfre  25199  dvmptres2  25209  dvmptntr  25218  dvcnvlem  25223  dvcnv  25224  dvferm1lem  25231  dvferm2lem  25233  dvlip  25240  dvlipcn  25241  dvlip2  25242  c1liplem1  25243  dvgt0lem1  25249  lhop1lem  25260  lhop  25263  dvcnvrelem1  25264  dvcnvrelem2  25265  dvcnvre  25266  dvfsumle  25268  dvfsumge  25269  dvfsumabs  25270  ftc1lem1  25282  ftc1lem2  25283  ftc1a  25284  ftc1lem4  25286  ftc2ditglem  25292  itgsubstlem  25295  ig1peu  25419  ig1pdvds  25424  taylfvallem1  25599  tayl0  25604  taylply2  25610  taylply  25611  dvtaylp  25612  dvntaylp  25613  dvntaylp0  25614  taylthlem1  25615  ulmdvlem1  25642  ulmdvlem3  25644  psercn  25668  pserdvlem2  25670  abelth  25683  xrlimcnp  26201  lgamucov  26270  wilthlem2  26301  sqff1o  26414  chtublem  26442  pntlemq  26832  pntlemf  26836  tglineintmo  27139  ttgcontlem1  27388  pthdlem1  28270  shintcli  29827  shub1  29880  mdslmd1lem1  30823  mdexchi  30833  chirredlem1  30888  mdsymlem5  30905  sumdmdii  30913  sumdmdlem2  30917  fnpreimac  31143  fsuppinisegfi  31156  xrsupssd  31217  xrge0infssd  31219  swrdrn3  31362  swrdf1  31363  swrdrndisj  31364  pwrssmgc  31413  xrge0tsmsd  31452  linds2eq  31714  elrspunidl  31745  mxidlprm  31779  ssmxidllem  31780  ssmxidl  31781  lbsdiflsp0  31847  dimkerim  31848  fedgmullem1  31850  fedgmullem2  31851  fedgmul  31852  smatrcl  31886  locfinreflem  31930  cmpcref  31940  zarclsun  31960  zarclsiin  31961  zarclssn  31963  zarcmplem  31971  pnfneige0  32041  esum2d  32201  insiga  32245  sssigagen2  32254  dynkin  32275  dya2iocnei  32389  omsmon  32405  carsgclctunlem1  32424  carsggect  32425  omsmeas  32430  ftc2re  32718  fdvneggt  32720  fdvnegge  32722  reprsuc  32735  reprss  32737  reprlt  32739  reprinfz1  32742  logdivsqrle  32770  hgt750lemb  32776  bnj906  33049  bnj1020  33084  bnj1137  33114  bnj1408  33155  bnj1452  33171  erdszelem7  33298  erdszelem8  33299  erdsze2lem1  33304  connpconn  33336  cvmliftmolem1  33382  cvmlift2lem1  33403  cvmlift2lem9  33412  cvmlift2lem10  33413  cvmlift3lem6  33425  cvmlift3lem7  33426  satfsschain  33465  ss2mcls  33669  sssslt1  34063  sssslt2  34064  scutbdaybnd  34083  scutbdaybnd2  34084  neibastop2lem  34623  fnemeet2  34630  fnejoin1  34631  ontgval  34694  unbdqndv1  34762  opnmbllem0  35885  ftc1anclem7  35928  ftc1anclem8  35929  ftc1anc  35930  sstotbnd2  36004  heiborlem1  36041  heiborlem8  36048  intidl  36259  lsmsat  37242  lssats  37246  lpssat  37247  lssatle  37249  lssat  37250  lsatcvatlem  37283  paddss12  38054  paddasslem17  38071  pmodlem1  38081  pmod1i  38083  pmodl42N  38086  elpcliN  38128  pclfinN  38135  polcon3N  38152  polcon2N  38154  paddunN  38162  pclfinclN  38185  poml5N  38189  osumcllem1N  38191  osumcllem2N  38192  osumcllem3N  38193  pl42lem2N  38215  pl42lem4N  38217  cdlemn5pre  39435  dihord1  39453  dihord2a  39454  dihord2b  39455  dihord5b  39494  dochss  39600  dochdmj1  39625  djhsumss  39642  djhunssN  39644  dochexmidlem2  39696  lclkrslem1  39772  lclkrslem2  39773  lcfrlem2  39778  aks4d1p4  40308  aks4d1p5  40309  aks4d1p7  40312  aks4d1p8  40316  sticksstones1  40326  elrfi  40732  ismrcd1  40736  istopclsd  40738  mrefg2  40745  aomclem2  41097  aomclem6  41101  hbtlem6  41171  hbt  41172  mptrcllem  41455  dfrcl2  41516  relexp0a  41558  trclimalb2  41568  frege81d  41589  k0004ss2  41996  imo72b2lem0  42010  imo72b2lem2  42012  imo72b2  42017  uzwo4  42835  ssin0  42837  ixpssmapc  42856  ssinc  42871  ssdec  42872  supxrre3  43113  uzfissfz  43114  ssuzfz  43137  supminfxr  43253  inficc  43322  ressiocsup  43342  ressioosup  43343  ressiooinf  43345  limccog  43411  limclner  43442  limsupres  43496  limsupresuz2  43500  limsupequzlem  43513  limsupvaluz2  43529  supcnvlimsup  43531  limsupgtlem  43568  liminfresuz2  43578  cncfmptssg  43662  cncfuni  43677  icccncfext  43678  dvresntr  43709  dvbdfbdioolem1  43719  dvdmsscn  43727  dvnxpaek  43733  dvnprodlem2  43738  stoweidlem59  43850  fourierdlem20  43918  fourierdlem42  43940  fourierdlem48  43945  fourierdlem49  43946  fourierdlem52  43949  fourierdlem58  43955  fourierdlem64  43961  fourierdlem73  43970  fourierdlem76  43973  fourierdlem80  43977  fourierdlem84  43981  fourierdlem93  43990  fourierdlem103  44000  fourierdlem104  44001  fourierdlem113  44010  etransclem18  44043  ioorrnopnlem  44095  salincl  44114  intsal  44119  fsumlesge0  44166  sge0cl  44170  sge0supre  44178  sge0less  44181  sge0split  44198  sge0seq  44235  caragensspw  44298  omessre  44299  caragendifcl  44303  caratheodorylem1  44315  0ome  44318  omess0  44323  caragencmpl  44324  hoicvr  44337  hoissrrn  44338  hoicvrrex  44345  ovnlecvr  44347  ovnsslelem  44349  ovnssle  44350  ovnsubaddlem1  44359  hoissrrn2  44367  hoidmv1lelem1  44380  hoidmvlelem1  44384  hoidmvlelem2  44385  hoidmvlelem4  44387  ovnlecvr2  44399  voncmpl  44410  hspmbl  44418  opnvonmbllem1  44421  ovolval5lem2  44442  ovolval5lem3  44443  vonioolem1  44469  pimdecfgtioc  44504  pimincfltioc  44505  pimdecfgtioo  44506  pimincfltioo  44507  issmflem  44516  cnfsmf  44529  incsmflem  44530  smfsssmf  44532  smfadd  44554  decsmflem  44555  smflim  44566  smfres  44579  smfmul  44584  smfpimbor1lem1  44587  smfco  44591  smfsuplem1  44600  smfsuplem3  44602  smflimsuplem1  44609  smflimsuplem4  44612  smflimsuplem7  44615  subsubmgm  45616  cnneiima  46475  seposep  46484  iscnrm3rlem4  46502  iscnrm3llem1  46508  lubsscl  46519  glbsscl  46520  toplatglb  46552  setrecsss  46671  elpglem1  46681