Theorem sstrd 3979

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

Syntax hints:   → wi 4   ⊆ wss 3938

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  sstrid  3980  sstrdi  3981  rabssrabd  4060  ssdif2d  4122  uniintsn  4915  funss  6376  fssxp  6536  knatar  7112  tfisi  7575  suppssov1  7864  suppssfv  7868  tposss  7895  tfrlem1  8014  omwordri  8200  oewordri  8220  oeeui  8230  oaabs2  8274  omopthlem1  8284  ecinxp  8374  sbthlem1  8629  dffi2  8889  hartogslem1  9008  cantnfcl  9132  cantnflt  9137  cantnfp1lem3  9145  cantnflem3  9156  cnfcom  9165  cnfcom3lem  9168  rankssb  9279  tskwe  9381  dfac12lem2  9572  dfac12lem3  9573  cfflb  9683  cfcof  9698  ssfin2  9744  hsmexlem4  9853  ttukeylem6  9938  ttukeylem7  9939  fpwwe2lem1  10055  fpwwe2lem8  10061  fpwwe2lem11  10064  fpwwe2lem12  10065  canthnumlem  10072  canthwelem  10074  canthwe  10075  canthp1lem2  10077  pwfseqlem5  10087  wunex2  10162  tsktrss  10185  inttsk  10198  uzwo3  12346  supicc  12889  supiccub  12890  supicclub  12891  ssfzunsnext  12955  seqsplit  13406  seqf1olem2a  13411  seqz  13421  swrdval2  14010  trrelssd  14335  rtrclreclem4  14422  sumss  15083  qshash  15184  incexc  15194  incexc2  15195  prodss  15303  rpnnen2lem11  15579  vdwlem1  16319  ramub1lem1  16364  imasaddvallem  16804  imasvscaf  16814  mrerintcl  16870  ismred2  16876  mremre  16877  mrcuni  16894  mressmrcd  16900  submrc  16901  mrissmrid  16914  mreexexlem2d  16918  isacs2  16926  isacs1i  16930  invss  17033  ssctr  17097  funcres2b  17169  isacs3lem  17778  acsfiindd  17789  acsmapd  17790  acsmap2d  17791  tsrdir  17850  subsubm  17983  gsumwspan  18013  subsubg  18304  subgint  18305  cntzidss  18470  symggen  18600  pmtrdifellem1  18606  pmtrdifellem2  18607  pgpssslw  18741  lsmless1x  18771  lsmless2x  18772  lsmless12  18789  subglsm  18801  gsumval3lem2  19028  gsumzaddlem  19043  gsumzadd  19044  gsum2d  19094  dmdprdd  19123  dprdfeq0  19146  dprdspan  19151  dprdres  19152  dprdss  19153  dprdz  19154  subgdmdprd  19158  subgdprd  19159  dprdsn  19160  dprd2dlem1  19165  dprd2da  19166  dmdprdsplit2lem  19169  dprdsplit  19172  pgpfac1lem2  19199  pgpfac1lem3  19201  pgpfac1lem5  19203  subsubrg  19563  subdrgint  19584  lspss  19758  lspun  19761  lsslsp  19789  lmhmlsp  19823  lsmelval2  19859  lsmssspx  19862  lsppratlem2  19922  lsppratlem3  19923  lsppratlem4  19924  lbsextlem2  19933  lbsextlem3  19934  aspss  20108  mhpaddcl  20340  mhpvscacl  20343  ocvlsp  20822  cssmre  20839  obselocv  20874  obslbs  20876  toponmre  21703  neiint  21714  neiss  21719  lpss  21752  lpss3  21754  restopnb  21785  restfpw  21789  neitr  21790  restcls  21791  restntr  21792  restlp  21793  ordtbas  21802  pnfnei  21830  mnfnei  21831  iscnp4  21873  cnclsi  21882  isreg2  21987  discmp  22008  cmpcld  22012  uncmp  22013  sscmp  22015  hauscmplem  22016  cmpfi  22018  iunconnlem  22037  clsconn  22040  2ndcctbss  22065  restnlly  22092  llyrest  22095  nllyrest  22096  llyidm  22098  nllyidm  22099  cldllycmp  22105  dislly  22107  comppfsc  22142  llycmpkgen2  22160  ptbasfi  22191  txnlly  22247  txcmplem1  22251  tx1stc  22260  xkococnlem  22269  qtopval2  22306  basqtop  22321  tgqtop  22322  qtoprest  22327  kqreglem1  22351  kqreglem2  22352  kqnrmlem1  22353  kqnrmlem2  22354  fsubbas  22477  fgabs  22489  fbasrn  22494  trfil2  22497  trfg  22501  isufil2  22518  trufil  22520  ssufl  22528  ufileu  22529  filufint  22530  fmfnfmlem4  22567  fmfnfm  22568  flimss2  22582  flimss1  22583  fclsfnflim  22637  flimfnfcls  22638  fclscmp  22640  cnpfcfi  22650  alexsubALT  22661  clssubg  22719  clsnsg  22720  tsmsres  22754  ustexsym  22826  ustex2sym  22827  ustex3sym  22828  ustneism  22834  trust  22840  utoptop  22845  restutopopn  22849  utop2nei  22861  utopreg  22863  cfiluweak  22906  neipcfilu  22907  blssps  23036  blss  23037  blcld  23117  blsscls  23119  met1stc  23133  met2ndci  23134  metust  23170  cfilucfil  23171  restmetu  23182  tgqioo  23410  xrsblre  23421  reconnlem2  23437  xrge0gsumle  23443  xrge0tsms  23444  rescncf  23507  cnmpopc  23534  cnheibor  23561  cnllycmp  23562  lebnum  23570  phtpycn  23589  cfilfcls  23879  iscmet3lem2  23897  cmetss  23921  cncmet  23927  bcthlem4  23932  bcth3  23936  rrxcph  23997  rrxmetlem  24012  minveclem4a  24035  minveclem4  24037  ivthicc  24061  ovollb  24082  ovollb2lem  24091  ovollb2  24092  nulmbl2  24139  ioorcl2  24175  uniioombllem3  24188  uniioombllem4  24189  uniioombllem5  24190  opnmbllem  24204  volcn  24209  volivth  24210  mbfeqalem1  24244  itg10a  24313  mbfi1fseqlem4  24321  ditgcl  24458  ditgswap  24459  ditgsplitlem  24460  limcflf  24481  limcres  24486  dvbss  24501  dvbsss  24502  perfdvf  24503  dvreslem  24509  dvres2lem  24510  dvres3  24513  dvcnp  24518  dvcnp2  24519  dvcn  24520  dvnff  24522  dvn2bss  24529  dvnres  24530  cpnord  24534  dvaddbr  24537  dvmulbr  24538  dvcobr  24545  dvnfre  24551  dvmptres2  24561  dvmptntr  24570  dvcnvlem  24575  dvcnv  24576  dvferm1lem  24583  dvferm2lem  24585  dvlip  24592  dvlipcn  24593  dvlip2  24594  c1liplem1  24595  dvgt0lem1  24601  lhop1lem  24612  lhop  24615  dvcnvrelem1  24616  dvcnvrelem2  24617  dvcnvre  24618  dvfsumle  24620  dvfsumge  24621  dvfsumabs  24622  ftc1lem1  24634  ftc1lem2  24635  ftc1a  24636  ftc1lem4  24638  ftc2ditglem  24644  itgsubstlem  24647  ig1peu  24767  ig1pdvds  24772  taylfvallem1  24947  tayl0  24952  taylply2  24958  taylply  24959  dvtaylp  24960  dvntaylp  24961  dvntaylp0  24962  taylthlem1  24963  ulmdvlem1  24990  ulmdvlem3  24992  psercn  25016  pserdvlem2  25018  abelth  25031  xrlimcnp  25548  lgamucov  25617  wilthlem2  25648  sqff1o  25761  chtublem  25789  pntlemq  26179  pntlemf  26183  tglineintmo  26430  ttgcontlem1  26673  pthdlem1  27549  shintcli  29108  shub1  29161  mdslmd1lem1  30104  mdexchi  30114  chirredlem1  30169  mdsymlem5  30186  sumdmdii  30194  sumdmdlem2  30198  fnpreimac  30418  xrsupssd  30485  xrge0infssd  30487  swrdrn3  30631  swrdf1  30632  swrdrndisj  30633  xrge0tsmsd  30694  linds2eq  30943  mxidlprm  30979  ssmxidllem  30980  ssmxidl  30981  lbsdiflsp0  31024  dimkerim  31025  fedgmullem1  31027  fedgmullem2  31028  fedgmul  31029  smatrcl  31063  locfinreflem  31106  cmpcref  31116  pnfneige0  31196  esum2d  31354  insiga  31398  sssigagen2  31407  dynkin  31428  dya2iocnei  31542  omsmon  31558  carsgclctunlem1  31577  carsggect  31578  omsmeas  31583  ftc2re  31871  fdvneggt  31873  fdvnegge  31875  reprsuc  31888  reprss  31890  reprlt  31892  reprinfz1  31895  logdivsqrle  31923  hgt750lemb  31929  bnj906  32204  bnj1020  32239  bnj1137  32269  bnj1408  32310  bnj1452  32326  erdszelem7  32446  erdszelem8  32447  erdsze2lem1  32452  connpconn  32484  cvmliftmolem1  32530  cvmlift2lem1  32551  cvmlift2lem9  32560  cvmlift2lem10  32561  cvmlift3lem6  32573  cvmlift3lem7  32574  satfsschain  32613  ss2mcls  32817  dftrpred3g  33074  frrlem8  33132  sssslt1  33262  sssslt2  33263  scutbdaybnd  33277  neibastop2lem  33710  fnemeet2  33717  fnejoin1  33718  ontgval  33781  unbdqndv1  33849  opnmbllem0  34930  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  sstotbnd2  35054  heiborlem1  35091  heiborlem8  35098  intidl  35309  lsmsat  36146  lssats  36150  lpssat  36151  lssatle  36153  lssat  36154  lsatcvatlem  36187  paddss12  36957  paddasslem17  36974  pmodlem1  36984  pmod1i  36986  pmodl42N  36989  elpcliN  37031  pclfinN  37038  polcon3N  37055  polcon2N  37057  paddunN  37065  pclfinclN  37088  poml5N  37092  osumcllem1N  37094  osumcllem2N  37095  osumcllem3N  37096  pl42lem2N  37118  pl42lem4N  37120  cdlemn5pre  38338  dihord1  38356  dihord2a  38357  dihord2b  38358  dihord5b  38397  dochss  38503  dochdmj1  38528  djhsumss  38545  djhunssN  38547  dochexmidlem2  38599  lclkrslem1  38675  lclkrslem2  38676  lcfrlem2  38681  elrfi  39298  ismrcd1  39302  istopclsd  39304  mrefg2  39311  aomclem2  39662  aomclem6  39666  hbtlem6  39736  hbt  39737  mptrcllem  39980  dfrcl2  40026  relexp0a  40068  trclimalb2  40078  frege81d  40099  k0004ss2  40509  imo72b2lem0  40523  imo72b2lem2  40525  imo72b2  40532  uzwo4  41322  ssin0  41324  ixpssmapc  41343  ssinc  41360  ssdec  41361  supxrre3  41600  uzfissfz  41601  ssuzfz  41624  supminfxr  41747  inficc  41817  ressiocsup  41837  ressioosup  41838  ressiooinf  41840  limccog  41908  limclner  41939  limsupres  41993  limsupresuz2  41997  limsupequzlem  42010  limsupvaluz2  42026  supcnvlimsup  42028  limsupgtlem  42065  liminfresuz2  42075  cncfmptssg  42160  cncfuni  42176  icccncfext  42177  dvresntr  42209  dvmptresicc  42211  dvbdfbdioolem1  42220  dvdmsscn  42228  dvnxpaek  42234  dvnprodlem2  42239  stoweidlem59  42351  fourierdlem20  42419  fourierdlem42  42441  fourierdlem48  42446  fourierdlem49  42447  fourierdlem52  42450  fourierdlem58  42456  fourierdlem64  42462  fourierdlem73  42471  fourierdlem76  42474  fourierdlem80  42478  fourierdlem84  42482  fourierdlem93  42491  fourierdlem103  42501  fourierdlem104  42502  fourierdlem113  42511  etransclem18  42544  ioorrnopnlem  42596  salincl  42615  intsal  42620  fsumlesge0  42666  sge0cl  42670  sge0supre  42678  sge0less  42681  sge0split  42698  sge0seq  42735  caragensspw  42798  omessre  42799  caragendifcl  42803  caratheodorylem1  42815  0ome  42818  omess0  42823  caragencmpl  42824  hoicvr  42837  hoissrrn  42838  hoicvrrex  42845  ovnlecvr  42847  ovnsslelem  42849  ovnssle  42850  ovnsubaddlem1  42859  hoissrrn2  42867  hoidmv1lelem1  42880  hoidmvlelem1  42884  hoidmvlelem2  42885  hoidmvlelem4  42887  ovnlecvr2  42899  voncmpl  42910  hspmbl  42918  opnvonmbllem1  42921  ovolval5lem2  42942  ovolval5lem3  42943  vonioolem1  42969  pimdecfgtioc  43000  pimincfltioc  43001  pimdecfgtioo  43002  pimincfltioo  43003  issmflem  43011  cnfsmf  43024  incsmflem  43025  smfsssmf  43027  smfadd  43048  decsmflem  43049  smflim  43060  smfres  43072  smfmul  43077  smfpimbor1lem1  43080  smfco  43084  smfsuplem1  43092  smfsuplem3  43094  smflimsuplem1  43101  smflimsuplem4  43104  smflimsuplem7  43107  subsubmgm  44071  setrecsss  44810  elpglem1  44820