Theorem sstrd 3969

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

Syntax hints:   → wi 4   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3943

This theorem is referenced by:  sstrid  3970  sstrdi  3971  rabssrabd  4058  ssdif2d  4123  uniintsn  4961  funss  6554  fssxp  6732  knatar  7349  tfisi  7852  suppssov1  8194  suppssov2  8195  suppssfv  8199  tposss  8224  frrlem8  8290  tfrlem1  8388  omwordri  8582  oewordri  8602  oeeui  8612  oaabs2  8659  omopthlem1  8669  ecinxp  8804  sbthlem1  9095  dffi2  9433  hartogslem1  9554  cantnfcl  9679  cantnflt  9684  cantnfp1lem3  9692  cantnflem3  9703  cnfcom  9712  cnfcom3lem  9715  ttrcltr  9728  rankssb  9860  tskwe  9962  dfac12lem2  10157  dfac12lem3  10158  cfflb  10271  cfcof  10286  ssfin2  10332  hsmexlem4  10441  ttukeylem6  10526  ttukeylem7  10527  fpwwe2lem1  10643  fpwwe2lem7  10649  fpwwe2lem10  10652  fpwwe2lem11  10653  canthnumlem  10660  canthwelem  10662  canthwe  10663  canthp1lem2  10665  pwfseqlem5  10675  wunex2  10750  tsktrss  10773  inttsk  10786  uzwo3  12957  xrsupssd  13347  supicc  13516  supiccub  13517  supicclub  13518  ssfzunsnext  13584  seqsplit  14051  seqf1olem2a  14056  seqz  14066  swrdval2  14662  trrelssd  14990  rtrclreclem4  15078  sumss  15738  qshash  15841  incexc  15851  incexc2  15852  prodss  15961  rpnnen2lem11  16240  vdwlem1  16999  ramub1lem1  17044  imasaddvallem  17541  imasvscaf  17551  mrerintcl  17607  ismred2  17613  mremre  17614  mrcuni  17631  mressmrcd  17637  submrc  17638  mrissmrid  17651  mreexexlem2d  17655  isacs2  17663  isacs1i  17667  invss  17772  ssctr  17836  funcres2b  17908  isacs3lem  18550  acsfiindd  18561  acsmapd  18562  acsmap2d  18563  tsrdir  18612  subsubmgm  18686  subsubm  18792  gsumwspan  18822  subsubg  19130  subgint  19131  cntzidss  19321  symggen  19449  pmtrdifellem1  19455  pmtrdifellem2  19456  pgpssslw  19593  lsmless1x  19623  lsmless2x  19624  lsmless12  19641  subglsm  19652  gsumval3lem2  19885  gsumzaddlem  19900  gsumzadd  19901  gsum2d  19951  dmdprdd  19980  dprdfeq0  20003  dprdspan  20008  dprdres  20009  dprdss  20010  dprdz  20011  subgdmdprd  20015  subgdprd  20016  dprdsn  20017  dprd2dlem1  20022  dprd2da  20023  dmdprdsplit2lem  20026  dprdsplit  20029  pgpfac1lem2  20056  pgpfac1lem3  20058  pgpfac1lem5  20060  subsubrng  20521  subsubrg  20556  subdrgint  20761  lspss  20939  lspun  20942  lsslsp  20970  lsslspOLD  20971  lmhmlsp  21005  lsmelval2  21041  lsmssspx  21044  lsppratlem2  21107  lsppratlem3  21108  lsppratlem4  21109  lbsextlem2  21118  lbsextlem3  21119  ocvlsp  21634  cssmre  21651  obselocv  21686  obslbs  21688  aspss  21835  mhpaddcl  22087  mhpinvcl  22088  mhpvscacl  22090  psdmullem  22101  toponmre  23029  neiint  23040  neiss  23045  lpss  23078  lpss3  23080  restopnb  23111  restfpw  23115  neitr  23116  restcls  23117  restntr  23118  restlp  23119  ordtbas  23128  pnfnei  23156  mnfnei  23157  iscnp4  23199  cnclsi  23208  isreg2  23313  discmp  23334  cmpcld  23338  uncmp  23339  sscmp  23341  hauscmplem  23342  cmpfi  23344  iunconnlem  23363  clsconn  23366  2ndcctbss  23391  restnlly  23418  llyrest  23421  nllyrest  23422  llyidm  23424  nllyidm  23425  cldllycmp  23431  dislly  23433  comppfsc  23468  llycmpkgen2  23486  ptbasfi  23517  txnlly  23573  txcmplem1  23577  tx1stc  23586  xkococnlem  23595  qtopval2  23632  basqtop  23647  tgqtop  23648  qtoprest  23653  kqreglem1  23677  kqreglem2  23678  kqnrmlem1  23679  kqnrmlem2  23680  fsubbas  23803  fgabs  23815  fbasrn  23820  trfil2  23823  trfg  23827  isufil2  23844  trufil  23846  ssufl  23854  ufileu  23855  filufint  23856  fmfnfmlem4  23893  fmfnfm  23894  flimss2  23908  flimss1  23909  fclsfnflim  23963  flimfnfcls  23964  fclscmp  23966  cnpfcfi  23976  alexsubALT  23987  clssubg  24045  clsnsg  24046  tsmsres  24080  ustexsym  24152  ustex2sym  24153  ustex3sym  24154  ustneism  24160  trust  24166  utoptop  24171  restutopopn  24175  utop2nei  24187  utopreg  24189  cfiluweak  24231  neipcfilu  24232  blssps  24361  blss  24362  blcld  24442  blsscls  24444  met1stc  24458  met2ndci  24459  metust  24495  cfilucfil  24496  restmetu  24507  tgqioo  24737  xrsblre  24749  reconnlem2  24765  xrge0gsumle  24771  xrge0tsms  24772  rescncf  24839  cnmpopc  24871  cnheibor  24903  cnllycmp  24904  lebnum  24912  phtpycn  24931  cfilfcls  25224  iscmet3lem2  25242  cmetss  25266  cncmet  25272  bcthlem4  25277  bcth3  25281  rrxcph  25342  rrxmetlem  25357  minveclem4a  25380  minveclem4  25382  ivthicc  25409  ovollb  25430  ovollb2lem  25439  ovollb2  25440  nulmbl2  25487  ioorcl2  25523  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  opnmbllem  25552  volcn  25557  volivth  25558  mbfeqalem1  25592  itg10a  25661  mbfi1fseqlem4  25669  ditgcl  25809  ditgswap  25810  ditgsplitlem  25811  limcflf  25832  limcres  25837  dvbss  25852  dvbsss  25853  perfdvf  25854  dvreslem  25860  dvres2lem  25861  dvres3  25864  dvmptresicc  25867  dvcnp  25870  dvcnp2  25871  dvcnp2OLD  25872  dvcn  25873  dvnff  25875  dvn2bss  25882  dvnres  25883  cpnord  25887  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcobr  25899  dvcobrOLD  25900  dvnfre  25906  dvmptres2  25916  dvmptntr  25925  dvcnvlem  25930  dvcnv  25931  dvferm1lem  25938  dvferm2lem  25940  dvlip  25948  dvlipcn  25949  dvlip2  25950  c1liplem1  25951  dvgt0lem1  25957  lhop1lem  25968  lhop  25971  dvcnvrelem1  25972  dvcnvrelem2  25973  dvcnvre  25974  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvfsumabs  25979  ftc1lem1  25992  ftc1lem2  25993  ftc1a  25994  ftc1lem4  25996  ftc2ditglem  26002  itgsubstlem  26005  ig1peu  26130  ig1pdvds  26135  taylfvallem1  26314  tayl0  26319  taylply2  26325  taylply2OLD  26326  taylply  26327  dvtaylp  26328  dvntaylp  26329  dvntaylp0  26330  taylthlem1  26331  ulmdvlem1  26359  ulmdvlem3  26361  psercn  26386  pserdvlem2  26388  abelth  26401  xrlimcnp  26928  lgamucov  26998  wilthlem2  27029  sqff1o  27142  chtublem  27172  pntlemq  27562  pntlemf  27566  sssslt1  27757  sssslt2  27758  scutbdaybnd  27777  scutbdaybnd2  27778  cofss  27881  coiniss  27882  tglineintmo  28567  ttgcontlem1  28810  pthdlem1  29694  shintcli  31256  shub1  31309  mdslmd1lem1  32252  mdexchi  32262  chirredlem1  32317  mdsymlem5  32334  sumdmdii  32342  sumdmdlem2  32346  fnpreimac  32595  fsuppinisegfi  32610  xrge0infssd  32684  swrdrn3  32877  swrdf1  32878  swrdrndisj  32879  pwrssmgc  32926  xrge0tsmsd  33002  elrgspnlem4  33186  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  fldgenss  33256  fldgenssp  33258  linds2eq  33342  elrspunidl  33389  ssdifidllem  33417  ssdifidlprm  33419  mxidlprm  33431  ssmxidllem  33434  ssmxidl  33435  qsdrnglem2  33457  rprmdvdsprod  33495  ressply1evls1  33524  resssra  33573  lsssra  33574  exsslsb  33582  lbsdiflsp0  33612  dimkerim  33613  fedgmullem1  33615  fedgmullem2  33616  fedgmul  33617  dimlssid  33618  fldextrspunlsplem  33660  fldextrspunlsp  33661  fldextrspunlem1  33662  fldextrspundgdvdslem  33667  fldextrspundgdvds  33668  constr01  33722  constrmon  33724  constrextdg2lem  33728  constrfiss  33731  smatrcl  33773  locfinreflem  33817  cmpcref  33827  zarclsun  33847  zarclsiin  33848  zarclssn  33850  zarcmplem  33858  pnfneige0  33928  esum2d  34070  insiga  34114  sssigagen2  34123  dynkin  34144  dya2iocnei  34260  omsmon  34276  carsgclctunlem1  34295  carsggect  34296  omsmeas  34301  ftc2re  34576  fdvneggt  34578  fdvnegge  34580  reprsuc  34593  reprss  34595  reprlt  34597  reprinfz1  34600  logdivsqrle  34628  hgt750lemb  34634  bnj906  34907  bnj1020  34942  bnj1137  34972  bnj1408  35013  bnj1452  35029  erdszelem7  35165  erdszelem8  35166  erdsze2lem1  35171  connpconn  35203  cvmliftmolem1  35249  cvmlift2lem1  35270  cvmlift2lem9  35279  cvmlift2lem10  35280  cvmlift3lem6  35292  cvmlift3lem7  35293  satfsschain  35332  ss2mcls  35536  neibastop2lem  36324  fnemeet2  36331  fnejoin1  36332  ontgval  36395  unbdqndv1  36472  opnmbllem0  37626  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  sstotbnd2  37744  heiborlem1  37781  heiborlem8  37788  intidl  37999  lsmsat  38972  lssats  38976  lpssat  38977  lssatle  38979  lssat  38980  lsatcvatlem  39013  paddss12  39784  paddasslem17  39801  pmodlem1  39811  pmod1i  39813  pmodl42N  39816  elpcliN  39858  pclfinN  39865  polcon3N  39882  polcon2N  39884  paddunN  39892  pclfinclN  39915  poml5N  39919  osumcllem1N  39921  osumcllem2N  39922  osumcllem3N  39923  pl42lem2N  39945  pl42lem4N  39947  cdlemn5pre  41165  dihord1  41183  dihord2a  41184  dihord2b  41185  dihord5b  41224  dochss  41330  dochdmj1  41355  djhsumss  41372  djhunssN  41374  dochexmidlem2  41426  lclkrslem1  41502  lclkrslem2  41503  lcfrlem2  41508  aks4d1p4  42038  aks4d1p5  42039  aks4d1p7  42042  aks4d1p8  42046  aks6d1c2  42089  sticksstones1  42105  unitscyglem5  42158  prjcrv0  42603  elrfi  42664  ismrcd1  42668  istopclsd  42670  mrefg2  42677  aomclem2  43026  aomclem6  43030  hbtlem6  43100  hbt  43101  oege2  43278  cantnftermord  43291  omabs2  43303  tfsconcat0b  43317  naddgeoa  43365  naddwordnexlem0  43367  naddwordnexlem1  43368  dfno2  43399  mptrcllem  43584  dfrcl2  43645  relexp0a  43687  trclimalb2  43697  frege81d  43718  k0004ss2  44123  imo72b2lem2  44138  imo72b2  44143  uzwo4  45025  ssin0  45027  ixpssmapc  45045  ssinc  45059  ssdec  45060  supxrre3  45300  uzfissfz  45301  ssuzfz  45324  supminfxr  45439  inficc  45511  ressiocsup  45531  ressioosup  45532  ressiooinf  45534  limccog  45597  limclner  45628  limsupres  45682  limsupresuz2  45686  limsupequzlem  45699  supcnvlimsup  45717  limsupgtlem  45754  liminfresuz2  45764  cncfmptssg  45848  cncfuni  45863  icccncfext  45864  dvresntr  45895  dvbdfbdioolem1  45905  dvdmsscn  45913  dvnxpaek  45919  dvnprodlem2  45924  stoweidlem59  46036  fourierdlem20  46104  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem52  46135  fourierdlem58  46141  fourierdlem64  46147  fourierdlem73  46156  fourierdlem76  46159  fourierdlem80  46163  fourierdlem84  46167  fourierdlem93  46176  fourierdlem103  46186  fourierdlem104  46187  fourierdlem113  46196  etransclem18  46229  ioorrnopnlem  46281  salincl  46301  intsal  46307  fsumlesge0  46354  sge0cl  46358  sge0supre  46366  sge0less  46369  sge0split  46386  sge0seq  46423  caragensspw  46486  omessre  46487  caragendifcl  46491  caratheodorylem1  46503  0ome  46506  omess0  46511  caragencmpl  46512  hoicvr  46525  hoissrrn  46526  hoicvrrex  46533  ovnlecvr  46535  ovnsslelem  46537  ovnssle  46538  ovnsubaddlem1  46547  hoissrrn2  46555  hoidmv1lelem1  46568  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem4  46575  ovnlecvr2  46587  voncmpl  46598  hspmbl  46606  opnvonmbllem1  46609  ovolval5lem2  46630  ovolval5lem3  46631  vonioolem1  46657  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  issmflem  46704  cnfsmf  46717  incsmflem  46718  smfsssmf  46720  smfadd  46742  decsmflem  46743  smflim  46754  smfres  46767  smfmul  46772  smfpimbor1lem1  46775  smfco  46779  smfsuplem1  46788  smfsuplem3  46790  smflimsuplem1  46797  smflimsuplem4  46800  smflimsuplem7  46803  cnneiima  48839  seposep  48848  iscnrm3rlem4  48865  iscnrm3llem1  48871  lubsscl  48882  glbsscl  48883  toplatglb  48923  setrecsss  49513  elpglem1  49523