Theorem sstrd 3864

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

Syntax hints:   → wi 4   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-in 3832  df-ss 3839

This theorem is referenced by:  syl5ss  3865  syl6ss  3866  rabssrabd  3944  ssdif2d  4006  uniintsn  4780  funss  6201  fssxp  6357  knatar  6927  tfisi  7383  suppssov1  7658  suppssfv  7662  tposss  7689  tfrlem1  7809  omwordri  7991  oewordri  8011  oeeui  8021  oaabs2  8064  omopthlem1  8074  ecinxp  8164  sbthlem1  8415  dffi2  8674  hartogslem1  8793  cantnfcl  8916  cantnflt  8921  cantnfp1lem3  8929  cantnflem3  8940  cnfcom  8949  cnfcom3lem  8952  rankssb  9063  tskwe  9165  dfac12lem2  9356  dfac12lem3  9357  cfflb  9471  cfcof  9486  ssfin2  9532  hsmexlem4  9641  ttukeylem6  9726  ttukeylem7  9727  fpwwe2lem1  9843  fpwwe2lem8  9849  fpwwe2lem11  9852  fpwwe2lem12  9853  canthnumlem  9860  canthwelem  9862  canthwe  9863  canthp1lem2  9865  pwfseqlem5  9875  wunex2  9950  tsktrss  9973  inttsk  9986  uzwo3  12150  supicc  12695  supiccub  12696  supicclub  12697  ssfzunsnext  12761  seqsplit  13211  seqf1olem2a  13216  seqz  13226  swrdval2  13799  trrelssd  14184  rtrclreclem4  14271  sumss  14931  qshash  15032  incexc  15042  incexc2  15043  prodss  15151  rpnnen2lem11  15427  vdwlem1  16163  ramub1lem1  16208  imasaddvallem  16648  imasvscaf  16658  mrerintcl  16716  ismred2  16722  mremre  16723  mrcuni  16740  mressmrcd  16746  submrc  16747  mrissmrid  16760  mreexexlem2d  16764  isacs2  16772  isacs1i  16776  invss  16879  ssctr  16943  funcres2b  17015  isacs3lem  17624  acsfiindd  17635  acsmapd  17636  acsmap2d  17637  tsrdir  17696  subsubm  17815  gsumwspan  17842  subsubg  18076  subgint  18077  cntzidss  18229  symggen  18349  pmtrdifellem1  18355  pmtrdifellem2  18356  pgpssslw  18490  lsmless1x  18520  lsmless2x  18521  lsmless12  18537  subglsm  18547  gsumval3lem2  18770  gsumzaddlem  18784  gsumzadd  18785  gsum2d  18835  dmdprdd  18861  dprdfeq0  18884  dprdspan  18889  dprdres  18890  dprdss  18891  dprdz  18892  subgdmdprd  18896  subgdprd  18897  dprdsn  18898  dprd2dlem1  18903  dprd2da  18904  dmdprdsplit2lem  18907  dprdsplit  18910  pgpfac1lem2  18937  pgpfac1lem3  18939  pgpfac1lem5  18941  subsubrg  19274  subdrgint  19294  lspss  19468  lspun  19471  lsslsp  19499  lmhmlsp  19533  lsmelval2  19569  lsmssspx  19572  lsppratlem2  19632  lsppratlem3  19633  lsppratlem4  19634  lbsextlem2  19643  lbsextlem3  19644  aspss  19816  mhpaddcl  20034  ocvlsp  20512  cssmre  20529  obselocv  20564  obslbs  20566  toponmre  21395  neiint  21406  neiss  21411  lpss  21444  lpss3  21446  restopnb  21477  restfpw  21481  neitr  21482  restcls  21483  restntr  21484  restlp  21485  ordtbas  21494  pnfnei  21522  mnfnei  21523  iscnp4  21565  cnclsi  21574  isreg2  21679  discmp  21700  cmpcld  21704  uncmp  21705  sscmp  21707  hauscmplem  21708  cmpfi  21710  iunconnlem  21729  clsconn  21732  2ndcctbss  21757  restnlly  21784  llyrest  21787  nllyrest  21788  llyidm  21790  nllyidm  21791  cldllycmp  21797  dislly  21799  comppfsc  21834  llycmpkgen2  21852  ptbasfi  21883  txnlly  21939  txcmplem1  21943  tx1stc  21952  xkococnlem  21961  qtopval2  21998  basqtop  22013  tgqtop  22014  qtoprest  22019  kqreglem1  22043  kqreglem2  22044  kqnrmlem1  22045  kqnrmlem2  22046  fsubbas  22169  fgabs  22181  fbasrn  22186  trfil2  22189  trfg  22193  isufil2  22210  trufil  22212  ssufl  22220  ufileu  22221  filufint  22222  fmfnfmlem4  22259  fmfnfm  22260  flimss2  22274  flimss1  22275  fclsfnflim  22329  flimfnfcls  22330  fclscmp  22332  cnpfcfi  22342  alexsubALT  22353  clssubg  22410  clsnsg  22411  tsmsres  22445  ustexsym  22517  ustex2sym  22518  ustex3sym  22519  ustneism  22525  trust  22531  utoptop  22536  restutopopn  22540  utop2nei  22552  utopreg  22554  cfiluweak  22597  neipcfilu  22598  blssps  22727  blss  22728  blcld  22808  blsscls  22810  met1stc  22824  met2ndci  22825  metust  22861  cfilucfil  22862  restmetu  22873  tgqioo  23101  xrsblre  23112  reconnlem2  23128  xrge0gsumle  23134  xrge0tsms  23135  rescncf  23198  cnmpopc  23225  cnheibor  23252  cnllycmp  23253  lebnum  23261  phtpycn  23280  cfilfcls  23570  iscmet3lem2  23588  cmetss  23612  cncmet  23618  bcthlem4  23623  bcth3  23627  rrxcph  23688  rrxmetlem  23703  minveclem4a  23726  minveclem4  23728  ivthicc  23752  ovollb  23773  ovollb2lem  23782  ovollb2  23783  nulmbl2  23830  ioorcl2  23866  uniioombllem3  23879  uniioombllem4  23880  uniioombllem5  23881  opnmbllem  23895  volcn  23900  volivth  23901  mbfeqalem1  23935  itg10a  24004  mbfi1fseqlem4  24012  ditgcl  24149  ditgswap  24150  ditgsplitlem  24151  limcflf  24172  limcres  24177  dvbss  24192  dvbsss  24193  perfdvf  24194  dvreslem  24200  dvres2lem  24201  dvres3  24204  dvcnp  24209  dvcnp2  24210  dvcn  24211  dvnff  24213  dvn2bss  24220  dvnres  24221  cpnord  24225  dvaddbr  24228  dvmulbr  24229  dvcobr  24236  dvnfre  24242  dvmptres2  24252  dvmptntr  24261  dvcnvlem  24266  dvcnv  24267  dvferm1lem  24274  dvferm2lem  24276  dvlip  24283  dvlipcn  24284  dvlip2  24285  c1liplem1  24286  dvgt0lem1  24292  lhop1lem  24303  lhop  24306  dvcnvrelem1  24307  dvcnvrelem2  24308  dvcnvre  24309  dvfsumle  24311  dvfsumge  24312  dvfsumabs  24313  ftc1lem1  24325  ftc1lem2  24326  ftc1a  24327  ftc1lem4  24329  ftc2ditglem  24335  itgsubstlem  24338  ig1peu  24458  ig1pdvds  24463  taylfvallem1  24638  tayl0  24643  taylply2  24649  taylply  24650  dvtaylp  24651  dvntaylp  24652  dvntaylp0  24653  taylthlem1  24654  ulmdvlem1  24681  ulmdvlem3  24683  psercn  24707  pserdvlem2  24709  abelth  24722  xrlimcnp  25238  lgamucov  25307  wilthlem2  25338  sqff1o  25451  chtublem  25479  pntlemq  25869  pntlemf  25873  tglineintmo  26120  ttgcontlem1  26364  pthdlem1  27245  shintcli  28877  shub1  28930  mdslmd1lem1  29873  mdexchi  29883  chirredlem1  29938  mdsymlem5  29955  sumdmdii  29963  sumdmdlem2  29967  fnpreimac  30168  xrsupssd  30224  xrge0infssd  30226  xrge0tsmsd  30486  linds2eq  30568  lbsdiflsp0  30607  dimkerim  30608  fedgmullem1  30610  fedgmullem2  30611  fedgmul  30612  smatrcl  30660  locfinreflem  30705  cmpcref  30715  pnfneige0  30795  esum2d  30953  insiga  30998  sssigagen2  31007  dynkin  31028  dya2iocnei  31142  omsmon  31158  carsgclctunlem1  31177  carsggect  31178  omsmeas  31183  ftc2re  31478  fdvneggt  31480  fdvnegge  31482  reprsuc  31495  reprss  31497  reprlt  31499  reprinfz1  31502  logdivsqrle  31530  hgt750lemb  31536  bnj906  31810  bnj1020  31843  bnj1137  31873  bnj1408  31914  bnj1452  31930  erdszelem7  31989  erdszelem8  31990  erdsze2lem1  31995  connpconn  32027  cvmliftmolem1  32073  cvmlift2lem1  32094  cvmlift2lem9  32103  cvmlift2lem10  32104  cvmlift3lem6  32116  cvmlift3lem7  32117  ss2mcls  32275  dftrpred3g  32533  frrlem8  32591  sssslt1  32721  sssslt2  32722  scutbdaybnd  32736  neibastop2lem  33169  fnemeet2  33176  fnejoin1  33177  ontgval  33239  unbdqndv1  33307  opnmbllem0  34317  ftc1anclem7  34362  ftc1anclem8  34363  ftc1anc  34364  sstotbnd2  34442  heiborlem1  34479  heiborlem8  34486  intidl  34697  lsmsat  35537  lssats  35541  lpssat  35542  lssatle  35544  lssat  35545  lsatcvatlem  35578  paddss12  36348  paddasslem17  36365  pmodlem1  36375  pmod1i  36377  pmodl42N  36380  elpcliN  36422  pclfinN  36429  polcon3N  36446  polcon2N  36448  paddunN  36456  pclfinclN  36479  poml5N  36483  osumcllem1N  36485  osumcllem2N  36486  osumcllem3N  36487  pl42lem2N  36509  pl42lem4N  36511  cdlemn5pre  37729  dihord1  37747  dihord2a  37748  dihord2b  37749  dihord5b  37788  dochss  37894  dochdmj1  37919  djhsumss  37936  djhunssN  37938  dochexmidlem2  37990  lclkrslem1  38066  lclkrslem2  38067  lcfrlem2  38072  elrfi  38631  ismrcd1  38635  istopclsd  38637  mrefg2  38644  aomclem2  38996  aomclem6  39000  hbtlem6  39070  hbt  39071  mptrcllem  39281  dfrcl2  39327  relexp0a  39369  trclimalb2  39379  frege81d  39400  k0004ss2  39810  imo72b2lem0  39825  imo72b2lem2  39827  imo72b2lem1  39831  imo72b2  39835  uzwo4  40679  ssin0  40681  ixpssmapc  40700  ssinc  40720  ssdec  40721  supxrre3  40968  uzfissfz  40969  ssuzfz  40992  supminfxr  41117  inficc  41187  ressiocsup  41207  ressioosup  41208  ressiooinf  41210  limccog  41278  limclner  41309  limsuppnfdlem  41359  limsupres  41363  limsupresuz2  41367  limsupequzlem  41380  limsupvaluz2  41396  supcnvlimsup  41398  limsupgtlem  41435  liminfresuz2  41445  cncfmptssg  41529  cncfuni  41545  icccncfext  41546  dvresntr  41578  dvmptresicc  41580  dvbdfbdioolem1  41589  dvdmsscn  41597  dvnxpaek  41603  dvnprodlem2  41608  stoweidlem59  41721  fourierdlem20  41789  fourierdlem42  41811  fourierdlem48  41816  fourierdlem49  41817  fourierdlem52  41820  fourierdlem58  41826  fourierdlem64  41832  fourierdlem73  41841  fourierdlem76  41844  fourierdlem80  41848  fourierdlem84  41852  fourierdlem93  41861  fourierdlem103  41871  fourierdlem104  41872  fourierdlem113  41881  etransclem18  41914  ioorrnopnlem  41966  salincl  41985  intsal  41990  fsumlesge0  42036  sge0cl  42040  sge0supre  42048  sge0less  42051  sge0split  42068  sge0seq  42105  caragensspw  42168  omessre  42169  caragendifcl  42173  caratheodorylem1  42185  0ome  42188  omess0  42193  caragencmpl  42194  hoicvr  42207  hoissrrn  42208  hoicvrrex  42215  ovnlecvr  42217  ovnsslelem  42219  ovnssle  42220  ovnsubaddlem1  42229  hoissrrn2  42237  hoidmv1lelem1  42250  hoidmvlelem1  42254  hoidmvlelem2  42255  hoidmvlelem4  42257  ovnlecvr2  42269  voncmpl  42280  hspmbl  42288  opnvonmbllem1  42291  ovolval5lem2  42312  ovolval5lem3  42313  vonioolem1  42339  pimdecfgtioc  42370  pimincfltioc  42371  pimdecfgtioo  42372  pimincfltioo  42373  issmflem  42381  cnfsmf  42394  incsmflem  42395  smfsssmf  42397  smfadd  42418  decsmflem  42419  smflim  42430  smfres  42442  smfmul  42447  smfpimbor1lem1  42450  smfco  42454  smfsuplem1  42462  smfsuplem3  42464  smflimsuplem1  42471  smflimsuplem4  42474  smflimsuplem7  42477  subsubmgm  43372  setrecsss  44110  elpglem1  44120