Theorem sstrd 3923

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

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

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 3901

This theorem is used by:  sstrid  3924  sstrdi  3925  rabssrabd  4011  ssdif2d  4087  uniintsn  4948  funss  6578  fssxp  6759  knatar  7390  tfisi  7894  suppssov1  8242  suppssov2  8243  suppssfv  8247  tposss  8272  frrlem8  8339  tfrlem1  8411  omwordri  8608  oewordri  8629  oeeui  8639  oaabs2  8686  omopthlem1  8696  ecinxp  8841  sbthlem1  9134  dffi2  9442  hartogslem1  9563  cantnfcl  9695  cantnflt  9700  cantnfp1lem3  9708  cantnflem3  9719  cnfcom  9728  cnfcom3lem  9731  ttrcltr  9744  rankssb  9889  rankval4b  9907  tskwe  10058  dfac12lem2  10250  dfac12lem3  10251  cfflb  10364  cfcof  10379  ssfin2  10425  hsmexlem4  10534  ttukeylem6  10619  ttukeylem7  10620  fpwwe2lem1  10743  fpwwe2lem7  10749  fpwwe2lem10  10752  fpwwe2lem11  10753  canthnumlem  10760  canthwelem  10762  canthwe  10763  canthp1lem2  10765  pwfseqlem5  10775  wunex2  10850  tsktrss  10873  inttsk  10886  uzwo3  13097  xrsupssd  13490  supicc  13659  supiccub  13660  supicclub  13661  ssfzunsnext  13730  seqsplit  14205  seqf1olem2a  14210  seqz  14220  swrdval2  14822  swrdf1  14827  swrdrn3  14830  trrelssd  15155  rtrclreclem4  15243  sumss  15919  qshash  16023  incexc  16035  incexc2  16036  prodss  16143  rpnnen2lem11  16421  vdwlem1  17188  ramub1lem1  17233  imasaddvallem  17730  imasvscaf  17740  mrerintcl  17796  ismred2  17802  mremre  17803  mrcuni  17824  mressmrcd  17830  submrc  17831  mrissmrid  17844  mreexexlem2d  17848  isacs2  17856  isacs1i  17860  invss  17965  ssctr  18029  funcres2b  18101  isacs3lem  18745  acsfiindd  18756  acsmapd  18757  acsmap2d  18758  tsrdir  18807  subsubmgm  18928  subsubm  19041  gsumwspan  19071  subsubg  19389  subgint  19390  cntzidss  19584  symggen  19714  pmtrdifellem1  19720  pmtrdifellem2  19721  pgpssslw  19858  lsmless1x  19888  lsmless2x  19889  lsmless12  19906  subglsm  19917  gsumval3lem2  20150  gsumzaddlem  20165  gsumzadd  20166  gsum2d  20216  dmdprdd  20245  dprdfeq0  20268  dprdspan  20273  dprdres  20274  dprdss  20275  dprdz  20276  subgdmdprd  20280  subgdprd  20281  dprdsn  20282  dprd2dlem1  20287  dprd2da  20288  dmdprdsplit2lem  20291  dprdsplit  20294  pgpfac1lem2  20321  pgpfac1lem3  20323  pgpfac1lem5  20325  subsubrng  20845  subsubrg  20880  subdrgint  21090  lspss  21289  lspun  21292  lsslsp  21320  lmhmlsp  21354  lsmelval2  21390  lsmssspx  21393  lsppratlem2  21456  lsppratlem3  21457  lsppratlem4  21458  lbsextlem2  21467  lbsextlem3  21468  ssdifidllem  21670  ssdifidlprm  21672  ocvlsp  22012  cssmre  22029  obselocv  22064  obslbs  22066  aspss  22214  mhpaddcl  22502  mhpinvcl  22503  mhpvscacl  22505  psdmullem  22516  toponmre  23441  neiint  23452  neiss  23457  lpss  23490  lpss3  23492  restopnb  23523  restfpw  23527  neitr  23528  restcls  23529  restntr  23530  restlp  23531  ordtbas  23540  pnfnei  23568  mnfnei  23569  iscnp4  23611  cnclsi  23620  isreg2  23725  discmp  23746  cmpcld  23750  uncmp  23751  sscmp  23753  hauscmplem  23754  cmpfi  23756  iunconnlem  23775  clsconn  23778  2ndcctbss  23804  restnlly  23831  llyrest  23834  nllyrest  23835  llyidm  23837  nllyidm  23838  cldllycmp  23844  dislly  23846  comppfsc  23881  llycmpkgen2  23899  ptbasfi  23930  txnlly  23986  txcmplem1  23990  tx1stc  23999  xkococnlem  24008  qtopval2  24045  basqtop  24060  tgqtop  24061  qtoprest  24066  kqreglem1  24090  kqreglem2  24091  kqnrmlem1  24092  kqnrmlem2  24093  fsubbas  24216  fgabs  24228  fbasrn  24233  trfil2  24236  trfg  24240  isufil2  24257  trufil  24259  ssufl  24267  ufileu  24268  filufint  24269  fmfnfmlem4  24306  fmfnfm  24307  flimss2  24321  flimss1  24322  fclsfnflim  24376  flimfnfcls  24377  fclscmp  24379  cnpfcfi  24389  alexsubALT  24400  clssubg  24458  clsnsg  24459  tsmsres  24493  ustexsym  24565  ustex2sym  24566  ustex3sym  24567  ustneism  24573  trust  24578  utoptop  24583  restutopopn  24587  utop2nei  24599  utopreg  24601  cfiluweak  24643  neipcfilu  24644  blssps  24773  blss  24774  blcld  24854  blsscls  24856  met1stc  24870  met2ndci  24871  metust  24907  cfilucfil  24908  restmetu  24919  tgqioo  25149  xrsblre  25161  reconnlem2  25177  xrge0gsumle  25183  xrge0tsms  25184  rescncf  25248  cnmpopc  25279  cnheibor  25306  cnllycmp  25307  lebnum  25315  phtpycn  25334  cfilfcls  25625  iscmet3lem2  25643  cmetss  25667  cncmet  25673  bcthlem4  25678  bcth3  25682  rrxcph  25743  rrxmetlem  25758  minveclem4a  25781  minveclem4  25783  ivthicc  25809  ovollb  25830  ovollb2lem  25839  ovollb2  25840  nulmbl2  25887  ioorcl2  25923  uniioombllem3  25936  uniioombllem4  25937  uniioombllem5  25938  opnmbllem  25952  volcn  25957  volivth  25958  mbfeqalem1  25992  itg10a  26061  mbfi1fseqlem4  26069  ditgcl  26208  ditgswap  26209  ditgsplitlem  26210  limcflf  26231  limcres  26236  dvbss  26251  dvbsss  26252  perfdvf  26253  dvreslem  26259  dvres2lem  26260  dvres3  26263  dvmptresicc  26266  dvcnp  26269  dvcnp2  26270  dvcn  26271  dvnff  26273  dvn2bss  26280  dvnres  26281  cpnord  26285  dvaddbr  26288  dvmulbr  26289  dvcobr  26296  dvnfre  26302  dvmptres2  26312  dvmptntr  26321  dvcnvlem  26326  dvcnv  26327  dvferm1lem  26334  dvferm2lem  26336  dvlip  26343  dvlipcn  26344  dvlip2  26345  c1liplem1  26346  dvgt0lem1  26352  lhop1lem  26363  lhop  26366  dvcnvrelem1  26367  dvcnvrelem2  26368  dvcnvre  26369  dvfsumle  26371  dvfsumge  26372  dvfsumabs  26373  ftc1lem1  26385  ftc1lem2  26386  ftc1a  26387  ftc1lem4  26389  ftc2ditglem  26395  itgsubstlem  26398  ig1peu  26523  ig1pdvds  26528  taylfvallem1  26714  tayl0  26719  taylply2  26725  taylply  26726  dvtaylp  26727  dvntaylp  26728  dvntaylp0  26729  taylthlem1  26730  ulmdvlem1  26757  ulmdvlem3  26759  psercn  26783  pserdvlem2  26785  abelth  26798  xrlimcnp  27326  lgamucov  27395  wilthlem2  27426  sqff1o  27539  chtublem  27568  pntlemq  27958  pntlemf  27962  ssslts1  28189  ssslts2  28190  cutbdaybnd  28211  cutbdaybnd2  28212  eqcuts3  28220  cofss  28346  coiniss  28347  bdaypw2bnd  28881  bdayfinbndlem1  28883  z12bdaylem2  28887  tglineintmo  29140  ttgcontlem1  29492  pthdlem1  30382  shintcli  31961  shub1  32014  mdslmd1lem1  32957  mdexchi  32967  chirredlem1  33022  mdsymlem5  33039  sumdmdii  33047  sumdmdlem2  33051  fnpreimac  33336  fsuppinisegfi  33351  xrge0infssd  33423  swrdrndisj  33588  pwrssmgc  33631  xrge0tsmsd  33704  elrgspnlem4  33876  elrgspnsubrunlem1  33878  elrgspnsubrunlem2  33879  fldgenss  33948  fldgenssp  33950  linds2eq  34006  elrspunidl  34048  mxidlprm  34065  ssmxidllem  34068  ssmxidl  34069  qsdrnglem2  34090  rprmdvdsprod  34136  ressply1evls1  34167  resssra  34289  lsssra  34290  exsslsb  34299  lbsdiflsp0  34328  dimkerim  34329  fedgmullem1  34331  fedgmullem2  34332  fedgmul  34333  dimlssid  34334  fldextrspunlsplem  34375  fldextrspunlsp  34376  fldextrspunlem1  34377  fldextrspundgdvdslem  34382  fldextrspundgdvds  34383  constr01  34444  constrmon  34446  constrextdg2lem  34450  constrfiss  34453  smatrcl  34498  locfinreflem  34542  cmpcref  34552  zarclsun  34572  zarclsiin  34573  zarclssn  34575  zarcmplem  34583  pnfneige0  34653  esum2d  34795  insiga  34840  sssigagen2  34849  dynkin  34870  dya2iocnei  34984  omsmon  35000  carsgclctunlem1  35019  carsggect  35020  omsmeas  35025  ftc2re  35297  fdvneggt  35299  fdvnegge  35301  reprsuc  35314  reprss  35316  reprlt  35318  reprinfz1  35321  logdivsqrle  35349  hgt750lemb  35355  bnj906  35630  bnj1020  35665  bnj1137  35695  bnj1408  35736  bnj1452  35752  abweex  35801  fineqvnttrclselem2  35890  erdszelem7  36129  erdszelem8  36130  erdsze2lem1  36135  connpconn  36167  cvmliftmolem1  36213  cvmlift2lem1  36234  cvmlift2lem9  36243  cvmlift2lem10  36244  cvmlift3lem6  36256  cvmlift3lem7  36257  satfsschain  36296  ss2mcls  36500  neibastop2lem  37326  fnemeet2  37333  fnejoin1  37334  ontgval  37397  ttcmin  37462  unbdqndv1  37552  opnmbllem0  38766  ftc1anclem7  38809  ftc1anclem8  38810  ftc1anc  38811  sstotbnd2  38900  heiborlem1  38937  heiborlem8  38944  intidl  39155  lsmsat  40257  lssats  40261  lpssat  40262  lssatle  40264  lssat  40265  lsatcvatlem  40298  paddss12  41068  paddasslem17  41085  pmodlem1  41095  pmod1i  41097  pmodl42N  41100  elpcliN  41142  pclfinN  41149  polcon3N  41166  polcon2N  41168  paddunN  41176  pclfinclN  41199  poml5N  41203  osumcllem1N  41205  osumcllem2N  41206  osumcllem3N  41207  pl42lem2N  41229  pl42lem4N  41231  cdlemn5pre  42449  dihord1  42467  dihord2a  42468  dihord2b  42469  dihord5b  42508  dochss  42614  dochdmj1  42639  djhsumss  42656  djhunssN  42658  dochexmidlem2  42710  lclkrslem1  42786  lclkrslem2  42787  lcfrlem2  42792  aks4d1p4  43321  aks4d1p5  43322  aks4d1p7  43325  aks4d1p8  43329  aks6d1c2  43372  sticksstones1  43388  unitscyglem5  43441  prjcrv0  43862  elrfi  43898  ismrcd1  43902  istopclsd  43904  mrefg2  43911  aomclem2  44250  aomclem6  44254  hbtlem6  44323  hbt  44324  oege2  44501  cantnftermord  44514  omabs2  44526  tfsconcat0b  44540  naddgeoa  44588  naddwordnexlem0  44590  naddwordnexlem1  44591  dfno2  44621  mptrcllem  44805  dfrcl2  44866  relexp0a  44908  trclimalb2  44918  frege81d  44939  k0004ss2  45344  imo72b2lem2  45359  imo72b2  45364  dmstructnn  46119  ishfstruct  46226  uzwo4  46275  ssin0  46277  ixpssmapc  46295  ssinc  46307  ssdec  46308  supxrre3  46542  uzfissfz  46543  ssuzfz  46566  supminfxr  46679  inficc  46751  ressiocsup  46771  ressioosup  46772  ressiooinf  46774  limccog  46837  limclner  46866  limsupres  46920  limsupresuz2  46924  limsupequzlem  46937  supcnvlimsup  46955  limsupgtlem  46992  liminfresuz2  47002  cncfmptssg  47086  icccncfext  47102  dvresntr  47133  dvbdfbdioolem1  47143  dvdmsscn  47151  dvnxpaek  47157  dvnprodlem2  47162  stoweidlem59  47274  fourierdlem20  47342  fourierdlem42  47364  fourierdlem48  47369  fourierdlem49  47370  fourierdlem52  47373  fourierdlem58  47379  fourierdlem64  47385  fourierdlem73  47394  fourierdlem76  47397  fourierdlem80  47401  fourierdlem84  47405  fourierdlem93  47414  fourierdlem103  47424  fourierdlem104  47425  fourierdlem113  47434  etransclem18  47467  ioorrnopnlem  47519  salincl  47539  intsal  47545  fsumlesge0  47592  sge0cl  47596  sge0supre  47604  sge0less  47607  sge0split  47624  sge0seq  47661  caragensspw  47724  omessre  47725  caragendifcl  47729  caratheodorylem1  47741  0ome  47744  omess0  47749  caragencmpl  47750  hoissrrn  47764  hoicvrrex  47771  ovnlecvr  47773  ovnsslelem  47775  ovnssle  47776  ovnsubaddlem1  47785  hoissrrn2  47793  hoidmv1lelem1  47806  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem4  47813  ovnlecvr2  47825  voncmpl  47836  hspmbl  47844  opnvonmbllem1  47847  ovolval5lem2  47868  ovolval5lem3  47869  vonioolem1  47895  pimdecfgtioc  47930  pimincfltioc  47931  pimdecfgtioo  47932  pimincfltioo  47933  issmflem  47942  cnfsmf  47955  incsmflem  47956  smfsssmf  47958  smfadd  47980  decsmflem  47981  smflim  47992  smfres  48005  smfmul  48010  smfpimbor1lem1  48013  smfco  48017  smfsuplem1  48026  smfsuplem3  48028  smflimsuplem1  48035  smflimsuplem4  48038  smflimsuplem7  48041  tmachlem-agreeprod  48152  nndivides2  48659  cnneiima  50236  seposep  50245  iscnrm3rlem4  50262  iscnrm3llem1  50268  lubsscl  50279  glbsscl  50280  toplatglb  50320  setrecsss  51074  elpglem1  51084