Theorem sstrd 3955

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

Syntax hints:   → wi 4   ⊆ wss 3913

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3930

This theorem is referenced by:  sstrid  3956  sstrdi  3957  rabssrabd  4045  ssdif2d  4110  uniintsn  4951  funss  6553  fssxp  6731  knatar  7353  tfisi  7851  suppssov1  8189  suppssov2  8190  suppssfv  8194  tposss  8219  frrlem8  8286  tfrlem1  8358  omwordri  8553  oewordri  8574  oeeui  8584  oaabs2  8631  omopthlem1  8641  ecinxp  8786  sbthlem1  9071  dffi2  9379  hartogslem1  9500  cantnfcl  9632  cantnflt  9637  cantnfp1lem3  9645  cantnflem3  9656  cnfcom  9665  cnfcom3lem  9668  ttrcltr  9681  rankssb  9816  tskwe  9932  dfac12lem2  10124  dfac12lem3  10125  cfflb  10239  cfcof  10254  ssfin2  10300  hsmexlem4  10409  ttukeylem6  10494  ttukeylem7  10495  fpwwe2lem1  10612  fpwwe2lem7  10618  fpwwe2lem10  10621  fpwwe2lem11  10622  canthnumlem  10629  canthwelem  10631  canthwe  10632  canthp1lem2  10634  pwfseqlem5  10644  wunex2  10719  tsktrss  10742  inttsk  10755  uzwo3  12963  xrsupssd  13355  supicc  13524  supiccub  13525  supicclub  13526  ssfzunsnext  13593  seqsplit  14067  seqf1olem2a  14072  seqz  14082  swrdval2  14680  trrelssd  15006  rtrclreclem4  15094  sumss  15771  qshash  15875  incexc  15887  incexc2  15888  prodss  15997  rpnnen2lem11  16276  vdwlem1  17037  ramub1lem1  17082  imasaddvallem  17579  imasvscaf  17589  mrerintcl  17645  ismred2  17651  mremre  17652  mrcuni  17673  mressmrcd  17679  submrc  17680  mrissmrid  17693  mreexexlem2d  17697  isacs2  17705  isacs1i  17709  invss  17814  ssctr  17878  funcres2b  17950  isacs3lem  18594  acsfiindd  18605  acsmapd  18606  acsmap2d  18607  tsrdir  18656  subsubmgm  18764  subsubm  18871  gsumwspan  18901  subsubg  19212  subgint  19213  cntzidss  19406  symggen  19536  pmtrdifellem1  19542  pmtrdifellem2  19543  pgpssslw  19680  lsmless1x  19710  lsmless2x  19711  lsmless12  19728  subglsm  19739  gsumval3lem2  19972  gsumzaddlem  19987  gsumzadd  19988  gsum2d  20038  dmdprdd  20067  dprdfeq0  20090  dprdspan  20095  dprdres  20096  dprdss  20097  dprdz  20098  subgdmdprd  20102  subgdprd  20103  dprdsn  20104  dprd2dlem1  20109  dprd2da  20110  dmdprdsplit2lem  20113  dprdsplit  20116  pgpfac1lem2  20143  pgpfac1lem3  20145  pgpfac1lem5  20147  subsubrng  20644  subsubrg  20679  subdrgint  20880  lspss  21079  lspun  21082  lsslsp  21110  lmhmlsp  21144  lsmelval2  21180  lsmssspx  21183  lsppratlem2  21246  lsppratlem3  21247  lsppratlem4  21248  lbsextlem2  21257  lbsextlem3  21258  ssdifidllem  21449  ssdifidlprm  21451  ocvlsp  21791  cssmre  21808  obselocv  21843  obslbs  21845  aspss  21991  mhpaddcl  22279  mhpinvcl  22280  mhpvscacl  22282  psdmullem  22293  toponmre  23215  neiint  23226  neiss  23231  lpss  23264  lpss3  23266  restopnb  23297  restfpw  23301  neitr  23302  restcls  23303  restntr  23304  restlp  23305  ordtbas  23314  pnfnei  23342  mnfnei  23343  iscnp4  23385  cnclsi  23394  isreg2  23499  discmp  23520  cmpcld  23524  uncmp  23525  sscmp  23527  hauscmplem  23528  cmpfi  23530  iunconnlem  23549  clsconn  23552  2ndcctbss  23577  restnlly  23604  llyrest  23607  nllyrest  23608  llyidm  23610  nllyidm  23611  cldllycmp  23617  dislly  23619  comppfsc  23654  llycmpkgen2  23672  ptbasfi  23703  txnlly  23759  txcmplem1  23763  tx1stc  23772  xkococnlem  23781  qtopval2  23818  basqtop  23833  tgqtop  23834  qtoprest  23839  kqreglem1  23863  kqreglem2  23864  kqnrmlem1  23865  kqnrmlem2  23866  fsubbas  23989  fgabs  24001  fbasrn  24006  trfil2  24009  trfg  24013  isufil2  24030  trufil  24032  ssufl  24040  ufileu  24041  filufint  24042  fmfnfmlem4  24079  fmfnfm  24080  flimss2  24094  flimss1  24095  fclsfnflim  24149  flimfnfcls  24150  fclscmp  24152  cnpfcfi  24162  alexsubALT  24173  clssubg  24231  clsnsg  24232  tsmsres  24266  ustexsym  24338  ustex2sym  24339  ustex3sym  24340  ustneism  24346  trust  24351  utoptop  24356  restutopopn  24360  utop2nei  24372  utopreg  24374  cfiluweak  24416  neipcfilu  24417  blssps  24546  blss  24547  blcld  24627  blsscls  24629  met1stc  24643  met2ndci  24644  metust  24680  cfilucfil  24681  restmetu  24692  tgqioo  24922  xrsblre  24934  reconnlem2  24950  xrge0gsumle  24956  xrge0tsms  24957  rescncf  25021  cnmpopc  25052  cnheibor  25079  cnllycmp  25080  lebnum  25088  phtpycn  25107  cfilfcls  25398  iscmet3lem2  25416  cmetss  25440  cncmet  25446  bcthlem4  25451  bcth3  25455  rrxcph  25516  rrxmetlem  25531  minveclem4a  25554  minveclem4  25556  ivthicc  25582  ovollb  25603  ovollb2lem  25612  ovollb2  25613  nulmbl2  25660  ioorcl2  25696  uniioombllem3  25709  uniioombllem4  25710  uniioombllem5  25711  opnmbllem  25725  volcn  25730  volivth  25731  mbfeqalem1  25765  itg10a  25834  mbfi1fseqlem4  25842  ditgcl  25982  ditgswap  25983  ditgsplitlem  25984  limcflf  26005  limcres  26010  dvbss  26025  dvbsss  26026  perfdvf  26027  dvreslem  26033  dvres2lem  26034  dvres3  26037  dvmptresicc  26040  dvcnp  26043  dvcnp2  26044  dvcn  26045  dvnff  26047  dvn2bss  26054  dvnres  26055  cpnord  26059  dvaddbr  26062  dvmulbr  26063  dvcobr  26070  dvnfre  26076  dvmptres2  26086  dvmptntr  26095  dvcnvlem  26100  dvcnv  26101  dvferm1lem  26108  dvferm2lem  26110  dvlip  26117  dvlipcn  26118  dvlip2  26119  c1liplem1  26120  dvgt0lem1  26126  lhop1lem  26137  lhop  26140  dvcnvrelem1  26141  dvcnvrelem2  26142  dvcnvre  26143  dvfsumle  26145  dvfsumge  26146  dvfsumabs  26147  ftc1lem1  26159  ftc1lem2  26160  ftc1a  26161  ftc1lem4  26163  ftc2ditglem  26169  itgsubstlem  26172  ig1peu  26297  ig1pdvds  26302  taylfvallem1  26482  tayl0  26487  taylply2  26493  taylply  26494  dvtaylp  26495  dvntaylp  26496  dvntaylp0  26497  taylthlem1  26498  ulmdvlem1  26525  ulmdvlem3  26527  psercn  26551  pserdvlem2  26553  abelth  26566  xrlimcnp  27095  lgamucov  27164  wilthlem2  27195  sqff1o  27308  chtublem  27337  pntlemq  27727  pntlemf  27731  ssslts1  27928  ssslts2  27929  cutbdaybnd  27950  cutbdaybnd2  27951  eqcuts3  27959  cofss  28085  coiniss  28086  bdaypw2bnd  28620  bdayfinbndlem1  28622  z12bdaylem2  28626  tglineintmo  28873  ttgcontlem1  29171  pthdlem1  30052  shintcli  31618  shub1  31671  mdslmd1lem1  32614  mdexchi  32624  chirredlem1  32679  mdsymlem5  32696  sumdmdii  32704  sumdmdlem2  32708  fnpreimac  32952  fsuppinisegfi  32969  xrge0infssd  33043  swrdrn3  33212  swrdf1  33213  swrdrndisj  33214  pwrssmgc  33257  xrge0tsmsd  33330  elrgspnlem4  33502  elrgspnsubrunlem1  33504  elrgspnsubrunlem2  33505  fldgenss  33576  fldgenssp  33578  linds2eq  33634  elrspunidl  33676  mxidlprm  33694  ssmxidllem  33697  ssmxidl  33698  qsdrnglem2  33719  rprmdvdsprod  33765  ressply1evls1  33796  resssra  33918  lsssra  33919  exsslsb  33928  lbsdiflsp0  33957  dimkerim  33958  fedgmullem1  33960  fedgmullem2  33961  fedgmul  33962  dimlssid  33963  fldextrspunlsplem  34004  fldextrspunlsp  34005  fldextrspunlem1  34006  fldextrspundgdvdslem  34011  fldextrspundgdvds  34012  constr01  34073  constrmon  34075  constrextdg2lem  34079  constrfiss  34082  smatrcl  34127  locfinreflem  34171  cmpcref  34181  zarclsun  34201  zarclsiin  34202  zarclssn  34204  zarcmplem  34212  pnfneige0  34282  esum2d  34424  insiga  34468  sssigagen2  34477  dynkin  34498  dya2iocnei  34613  omsmon  34629  carsgclctunlem1  34648  carsggect  34649  omsmeas  34654  ftc2re  34926  fdvneggt  34928  fdvnegge  34930  reprsuc  34943  reprss  34945  reprlt  34947  reprinfz1  34950  logdivsqrle  34978  hgt750lemb  34984  bnj906  35259  bnj1020  35294  bnj1137  35324  bnj1408  35365  bnj1452  35381  rankval4b  35432  fineqvnttrclselem2  35454  erdszelem7  35584  erdszelem8  35585  erdsze2lem1  35590  connpconn  35622  cvmliftmolem1  35668  cvmlift2lem1  35689  cvmlift2lem9  35698  cvmlift2lem10  35699  cvmlift3lem6  35711  cvmlift3lem7  35712  satfsschain  35751  ss2mcls  35955  neibastop2lem  36756  fnemeet2  36763  fnejoin1  36764  ontgval  36827  ttcmin  36892  unbdqndv1  36982  opnmbllem0  38190  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  sstotbnd2  38308  heiborlem1  38345  heiborlem8  38352  intidl  38563  lsmsat  39667  lssats  39671  lpssat  39672  lssatle  39674  lssat  39675  lsatcvatlem  39708  paddss12  40478  paddasslem17  40495  pmodlem1  40505  pmod1i  40507  pmodl42N  40510  elpcliN  40552  pclfinN  40559  polcon3N  40576  polcon2N  40578  paddunN  40586  pclfinclN  40609  poml5N  40613  osumcllem1N  40615  osumcllem2N  40616  osumcllem3N  40617  pl42lem2N  40639  pl42lem4N  40641  cdlemn5pre  41859  dihord1  41877  dihord2a  41878  dihord2b  41879  dihord5b  41918  dochss  42024  dochdmj1  42049  djhsumss  42066  djhunssN  42068  dochexmidlem2  42120  lclkrslem1  42196  lclkrslem2  42197  lcfrlem2  42202  aks4d1p4  42731  aks4d1p5  42732  aks4d1p7  42735  aks4d1p8  42739  aks6d1c2  42782  sticksstones1  42798  unitscyglem5  42851  prjcrv0  43252  elrfi  43312  ismrcd1  43316  istopclsd  43318  mrefg2  43325  aomclem2  43669  aomclem6  43673  hbtlem6  43743  hbt  43744  oege2  43921  cantnftermord  43934  omabs2  43946  tfsconcat0b  43960  naddgeoa  44008  naddwordnexlem0  44010  naddwordnexlem1  44011  dfno2  44041  mptrcllem  44226  dfrcl2  44287  relexp0a  44329  trclimalb2  44339  frege81d  44360  k0004ss2  44765  imo72b2lem2  44780  imo72b2  44785  uzwo4  45660  ssin0  45662  ixpssmapc  45680  ssinc  45692  ssdec  45693  supxrre3  45928  uzfissfz  45929  ssuzfz  45952  supminfxr  46065  inficc  46137  ressiocsup  46157  ressioosup  46158  ressiooinf  46160  limccog  46223  limclner  46252  limsupres  46306  limsupresuz2  46310  limsupequzlem  46323  supcnvlimsup  46341  limsupgtlem  46378  liminfresuz2  46388  cncfmptssg  46472  icccncfext  46488  dvresntr  46519  dvbdfbdioolem1  46529  dvdmsscn  46537  dvnxpaek  46543  dvnprodlem2  46548  stoweidlem59  46660  fourierdlem20  46728  fourierdlem42  46750  fourierdlem48  46755  fourierdlem49  46756  fourierdlem52  46759  fourierdlem58  46765  fourierdlem64  46771  fourierdlem73  46780  fourierdlem76  46783  fourierdlem80  46787  fourierdlem84  46791  fourierdlem93  46800  fourierdlem103  46810  fourierdlem104  46811  fourierdlem113  46820  etransclem18  46853  ioorrnopnlem  46905  salincl  46925  intsal  46931  fsumlesge0  46978  sge0cl  46982  sge0supre  46990  sge0less  46993  sge0split  47010  sge0seq  47047  caragensspw  47110  omessre  47111  caragendifcl  47115  caratheodorylem1  47127  0ome  47130  omess0  47135  caragencmpl  47136  hoissrrn  47150  hoicvrrex  47157  ovnlecvr  47159  ovnsslelem  47161  ovnssle  47162  ovnsubaddlem1  47171  hoissrrn2  47179  hoidmv1lelem1  47192  hoidmvlelem1  47196  hoidmvlelem2  47197  hoidmvlelem4  47199  ovnlecvr2  47211  voncmpl  47222  hspmbl  47230  opnvonmbllem1  47233  ovolval5lem2  47254  ovolval5lem3  47255  vonioolem1  47281  pimdecfgtioc  47316  pimincfltioc  47317  pimdecfgtioo  47318  pimincfltioo  47319  issmflem  47328  cnfsmf  47341  incsmflem  47342  smfsssmf  47344  smfadd  47366  decsmflem  47367  smflim  47378  smfres  47391  smfmul  47396  smfpimbor1lem1  47399  smfco  47403  smfsuplem1  47412  smfsuplem3  47414  smflimsuplem1  47421  smflimsuplem4  47424  smflimsuplem7  47427  nndivides2  48005  cnneiima  49575  seposep  49584  iscnrm3rlem4  49601  iscnrm3llem1  49607  lubsscl  49618  glbsscl  49619  toplatglb  49659  setrecsss  50359  elpglem1  50369