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 596	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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

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

This theorem is used by:  sstrid  3942  sstrdi  3943  rabssrabd  4031  ssdif2d  4095  uniintsn  4945  funss  6550  fssxp  6729  knatar  7359  tfisi  7859  suppssov1  8198  suppssov2  8199  suppssfv  8203  tposss  8228  frrlem8  8295  tfrlem1  8367  omwordri  8564  oewordri  8585  oeeui  8595  oaabs2  8642  omopthlem1  8652  ecinxp  8797  sbthlem1  9090  dffi2  9399  hartogslem1  9520  cantnfcl  9652  cantnflt  9657  cantnfp1lem3  9665  cantnflem3  9676  cnfcom  9685  cnfcom3lem  9688  ttrcltr  9701  rankssb  9843  rankval4b  9861  tskwe  10012  dfac12lem2  10204  dfac12lem3  10205  cfflb  10318  cfcof  10333  ssfin2  10379  hsmexlem4  10488  ttukeylem6  10573  ttukeylem7  10574  fpwwe2lem1  10697  fpwwe2lem7  10703  fpwwe2lem10  10706  fpwwe2lem11  10707  canthnumlem  10714  canthwelem  10716  canthwe  10717  canthp1lem2  10719  pwfseqlem5  10729  wunex2  10804  tsktrss  10827  inttsk  10840  uzwo3  13051  xrsupssd  13444  supicc  13613  supiccub  13614  supicclub  13615  ssfzunsnext  13683  seqsplit  14158  seqf1olem2a  14163  seqz  14173  swrdval2  14774  swrdf1  14779  swrdrn3  14782  trrelssd  15106  rtrclreclem4  15194  sumss  15870  qshash  15974  incexc  15986  incexc2  15987  prodss  16094  rpnnen2lem11  16372  vdwlem1  17139  ramub1lem1  17184  imasaddvallem  17681  imasvscaf  17691  mrerintcl  17747  ismred2  17753  mremre  17754  mrcuni  17775  mressmrcd  17781  submrc  17782  mrissmrid  17795  mreexexlem2d  17799  isacs2  17807  isacs1i  17811  invss  17916  ssctr  17980  funcres2b  18052  isacs3lem  18696  acsfiindd  18707  acsmapd  18708  acsmap2d  18709  tsrdir  18758  subsubmgm  18879  subsubm  18992  gsumwspan  19022  subsubg  19340  subgint  19341  cntzidss  19534  symggen  19664  pmtrdifellem1  19670  pmtrdifellem2  19671  pgpssslw  19808  lsmless1x  19838  lsmless2x  19839  lsmless12  19856  subglsm  19867  gsumval3lem2  20100  gsumzaddlem  20115  gsumzadd  20116  gsum2d  20166  dmdprdd  20195  dprdfeq0  20218  dprdspan  20223  dprdres  20224  dprdss  20225  dprdz  20226  subgdmdprd  20230  subgdprd  20231  dprdsn  20232  dprd2dlem1  20237  dprd2da  20238  dmdprdsplit2lem  20241  dprdsplit  20244  pgpfac1lem2  20271  pgpfac1lem3  20273  pgpfac1lem5  20275  subsubrng  20795  subsubrg  20830  subdrgint  21040  lspss  21239  lspun  21242  lsslsp  21270  lmhmlsp  21304  lsmelval2  21340  lsmssspx  21343  lsppratlem2  21406  lsppratlem3  21407  lsppratlem4  21408  lbsextlem2  21417  lbsextlem3  21418  ssdifidllem  21620  ssdifidlprm  21622  ocvlsp  21962  cssmre  21979  obselocv  22014  obslbs  22016  aspss  22164  mhpaddcl  22452  mhpinvcl  22453  mhpvscacl  22455  psdmullem  22466  toponmre  23391  neiint  23402  neiss  23407  lpss  23440  lpss3  23442  restopnb  23473  restfpw  23477  neitr  23478  restcls  23479  restntr  23480  restlp  23481  ordtbas  23490  pnfnei  23518  mnfnei  23519  iscnp4  23561  cnclsi  23570  isreg2  23675  discmp  23696  cmpcld  23700  uncmp  23701  sscmp  23703  hauscmplem  23704  cmpfi  23706  iunconnlem  23725  clsconn  23728  2ndcctbss  23754  restnlly  23781  llyrest  23784  nllyrest  23785  llyidm  23787  nllyidm  23788  cldllycmp  23794  dislly  23796  comppfsc  23831  llycmpkgen2  23849  ptbasfi  23880  txnlly  23936  txcmplem1  23940  tx1stc  23949  xkococnlem  23958  qtopval2  23995  basqtop  24010  tgqtop  24011  qtoprest  24016  kqreglem1  24040  kqreglem2  24041  kqnrmlem1  24042  kqnrmlem2  24043  fsubbas  24166  fgabs  24178  fbasrn  24183  trfil2  24186  trfg  24190  isufil2  24207  trufil  24209  ssufl  24217  ufileu  24218  filufint  24219  fmfnfmlem4  24256  fmfnfm  24257  flimss2  24271  flimss1  24272  fclsfnflim  24326  flimfnfcls  24327  fclscmp  24329  cnpfcfi  24339  alexsubALT  24350  clssubg  24408  clsnsg  24409  tsmsres  24443  ustexsym  24515  ustex2sym  24516  ustex3sym  24517  ustneism  24523  trust  24528  utoptop  24533  restutopopn  24537  utop2nei  24549  utopreg  24551  cfiluweak  24593  neipcfilu  24594  blssps  24723  blss  24724  blcld  24804  blsscls  24806  met1stc  24820  met2ndci  24821  metust  24857  cfilucfil  24858  restmetu  24869  tgqioo  25099  xrsblre  25111  reconnlem2  25127  xrge0gsumle  25133  xrge0tsms  25134  rescncf  25198  cnmpopc  25229  cnheibor  25256  cnllycmp  25257  lebnum  25265  phtpycn  25284  cfilfcls  25575  iscmet3lem2  25593  cmetss  25617  cncmet  25623  bcthlem4  25628  bcth3  25632  rrxcph  25693  rrxmetlem  25708  minveclem4a  25731  minveclem4  25733  ivthicc  25759  ovollb  25780  ovollb2lem  25789  ovollb2  25790  nulmbl2  25837  ioorcl2  25873  uniioombllem3  25886  uniioombllem4  25887  uniioombllem5  25888  opnmbllem  25902  volcn  25907  volivth  25908  mbfeqalem1  25942  itg10a  26011  mbfi1fseqlem4  26019  ditgcl  26158  ditgswap  26159  ditgsplitlem  26160  limcflf  26181  limcres  26186  dvbss  26201  dvbsss  26202  perfdvf  26203  dvreslem  26209  dvres2lem  26210  dvres3  26213  dvmptresicc  26216  dvcnp  26219  dvcnp2  26220  dvcn  26221  dvnff  26223  dvn2bss  26230  dvnres  26231  cpnord  26235  dvaddbr  26238  dvmulbr  26239  dvcobr  26246  dvnfre  26252  dvmptres2  26262  dvmptntr  26271  dvcnvlem  26276  dvcnv  26277  dvferm1lem  26284  dvferm2lem  26286  dvlip  26293  dvlipcn  26294  dvlip2  26295  c1liplem1  26296  dvgt0lem1  26302  lhop1lem  26313  lhop  26316  dvcnvrelem1  26317  dvcnvrelem2  26318  dvcnvre  26319  dvfsumle  26321  dvfsumge  26322  dvfsumabs  26323  ftc1lem1  26335  ftc1lem2  26336  ftc1a  26337  ftc1lem4  26339  ftc2ditglem  26345  itgsubstlem  26348  ig1peu  26473  ig1pdvds  26478  taylfvallem1  26666  tayl0  26671  taylply2  26677  taylply  26678  dvtaylp  26679  dvntaylp  26680  dvntaylp0  26681  taylthlem1  26682  ulmdvlem1  26709  ulmdvlem3  26711  psercn  26735  pserdvlem2  26737  abelth  26750  xrlimcnp  27278  lgamucov  27347  wilthlem2  27378  sqff1o  27491  chtublem  27520  pntlemq  27910  pntlemf  27914  ssslts1  28141  ssslts2  28142  cutbdaybnd  28163  cutbdaybnd2  28164  eqcuts3  28172  cofss  28298  coiniss  28299  bdaypw2bnd  28833  bdayfinbndlem1  28835  z12bdaylem2  28839  tglineintmo  29092  ttgcontlem1  29444  pthdlem1  30334  shintcli  31913  shub1  31966  mdslmd1lem1  32909  mdexchi  32919  chirredlem1  32974  mdsymlem5  32991  sumdmdii  32999  sumdmdlem2  33003  fnpreimac  33246  fsuppinisegfi  33262  xrge0infssd  33335  swrdrndisj  33500  pwrssmgc  33543  xrge0tsmsd  33616  elrgspnlem4  33788  elrgspnsubrunlem1  33790  elrgspnsubrunlem2  33791  fldgenss  33860  fldgenssp  33862  linds2eq  33918  elrspunidl  33960  mxidlprm  33977  ssmxidllem  33980  ssmxidl  33981  qsdrnglem2  34002  rprmdvdsprod  34048  ressply1evls1  34079  resssra  34201  lsssra  34202  exsslsb  34211  lbsdiflsp0  34240  dimkerim  34241  fedgmullem1  34243  fedgmullem2  34244  fedgmul  34245  dimlssid  34246  fldextrspunlsplem  34287  fldextrspunlsp  34288  fldextrspunlem1  34289  fldextrspundgdvdslem  34294  fldextrspundgdvds  34295  constr01  34356  constrmon  34358  constrextdg2lem  34362  constrfiss  34365  smatrcl  34410  locfinreflem  34454  cmpcref  34464  zarclsun  34484  zarclsiin  34485  zarclssn  34487  zarcmplem  34495  pnfneige0  34565  esum2d  34707  insiga  34752  sssigagen2  34761  dynkin  34782  dya2iocnei  34897  omsmon  34913  carsgclctunlem1  34932  carsggect  34933  omsmeas  34938  ftc2re  35210  fdvneggt  35212  fdvnegge  35214  reprsuc  35227  reprss  35229  reprlt  35231  reprinfz1  35234  logdivsqrle  35262  hgt750lemb  35268  bnj906  35543  bnj1020  35578  bnj1137  35608  bnj1408  35649  bnj1452  35665  fineqvnttrclselem2  35763  erdszelem7  35931  erdszelem8  35932  erdsze2lem1  35937  connpconn  35969  cvmliftmolem1  36015  cvmlift2lem1  36036  cvmlift2lem9  36045  cvmlift2lem10  36046  cvmlift3lem6  36058  cvmlift3lem7  36059  satfsschain  36098  ss2mcls  36302  neibastop2lem  37118  fnemeet2  37125  fnejoin1  37126  ontgval  37189  ttcmin  37254  unbdqndv1  37344  opnmbllem0  38542  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  sstotbnd2  38676  heiborlem1  38713  heiborlem8  38720  intidl  38931  lsmsat  40033  lssats  40037  lpssat  40038  lssatle  40040  lssat  40041  lsatcvatlem  40074  paddss12  40844  paddasslem17  40861  pmodlem1  40871  pmod1i  40873  pmodl42N  40876  elpcliN  40918  pclfinN  40925  polcon3N  40942  polcon2N  40944  paddunN  40952  pclfinclN  40975  poml5N  40979  osumcllem1N  40981  osumcllem2N  40982  osumcllem3N  40983  pl42lem2N  41005  pl42lem4N  41007  cdlemn5pre  42225  dihord1  42243  dihord2a  42244  dihord2b  42245  dihord5b  42284  dochss  42390  dochdmj1  42415  djhsumss  42432  djhunssN  42434  dochexmidlem2  42486  lclkrslem1  42562  lclkrslem2  42563  lcfrlem2  42568  aks4d1p4  43097  aks4d1p5  43098  aks4d1p7  43101  aks4d1p8  43105  aks6d1c2  43148  sticksstones1  43164  unitscyglem5  43217  prjcrv0  43623  elrfi  43658  ismrcd1  43662  istopclsd  43664  mrefg2  43671  aomclem2  44015  aomclem6  44019  hbtlem6  44089  hbt  44090  oege2  44267  cantnftermord  44280  omabs2  44292  tfsconcat0b  44306  naddgeoa  44354  naddwordnexlem0  44356  naddwordnexlem1  44357  dfno2  44387  mptrcllem  44572  dfrcl2  44633  relexp0a  44675  trclimalb2  44685  frege81d  44706  k0004ss2  45111  imo72b2lem2  45126  imo72b2  45131  uzwo4  46013  ssin0  46015  ixpssmapc  46033  ssinc  46045  ssdec  46046  supxrre3  46281  uzfissfz  46282  ssuzfz  46305  supminfxr  46418  inficc  46490  ressiocsup  46510  ressioosup  46511  ressiooinf  46513  limccog  46576  limclner  46605  limsupres  46659  limsupresuz2  46663  limsupequzlem  46676  supcnvlimsup  46694  limsupgtlem  46731  liminfresuz2  46741  cncfmptssg  46825  icccncfext  46841  dvresntr  46872  dvbdfbdioolem1  46882  dvdmsscn  46890  dvnxpaek  46896  dvnprodlem2  46901  stoweidlem59  47013  fourierdlem20  47081  fourierdlem42  47103  fourierdlem48  47108  fourierdlem49  47109  fourierdlem52  47112  fourierdlem58  47118  fourierdlem64  47124  fourierdlem73  47133  fourierdlem76  47136  fourierdlem80  47140  fourierdlem84  47144  fourierdlem93  47153  fourierdlem103  47163  fourierdlem104  47164  fourierdlem113  47173  etransclem18  47206  ioorrnopnlem  47258  salincl  47278  intsal  47284  fsumlesge0  47331  sge0cl  47335  sge0supre  47343  sge0less  47346  sge0split  47363  sge0seq  47400  caragensspw  47463  omessre  47464  caragendifcl  47468  caratheodorylem1  47480  0ome  47483  omess0  47488  caragencmpl  47489  hoissrrn  47503  hoicvrrex  47510  ovnlecvr  47512  ovnsslelem  47514  ovnssle  47515  ovnsubaddlem1  47524  hoissrrn2  47532  hoidmv1lelem1  47545  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem4  47552  ovnlecvr2  47564  voncmpl  47575  hspmbl  47583  opnvonmbllem1  47586  ovolval5lem2  47607  ovolval5lem3  47608  vonioolem1  47634  pimdecfgtioc  47669  pimincfltioc  47670  pimdecfgtioo  47671  pimincfltioo  47672  issmflem  47681  cnfsmf  47694  incsmflem  47695  smfsssmf  47697  smfadd  47719  decsmflem  47720  smflim  47731  smfres  47744  smfmul  47749  smfpimbor1lem1  47752  smfco  47756  smfsuplem1  47765  smfsuplem3  47767  smflimsuplem1  47774  smflimsuplem4  47777  smflimsuplem7  47780  tmachlem-agreeprod  47891  nndivides2  48398  cnneiima  49969  seposep  49978  iscnrm3rlem4  49995  iscnrm3llem1  50001  lubsscl  50012  glbsscl  50013  toplatglb  50053  setrecsss  50738  elpglem1  50748