Theorem sstrd 3987

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

Syntax hints:   → wi 4   ⊆ wss 3944

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ss 3961

This theorem is referenced by:  sstrid  3988  sstrdi  3989  rabssrabd  4077  ssdif2d  4140  uniintsn  4991  funss  6573  fssxp  6751  knatar  7364  tfisi  7864  suppssov1  8203  suppssov2  8204  suppssfv  8208  tposss  8233  frrlem8  8299  tfrlem1  8397  omwordri  8593  oewordri  8613  oeeui  8623  oaabs2  8670  omopthlem1  8680  ecinxp  8811  sbthlem1  9108  dffi2  9448  hartogslem1  9567  cantnfcl  9692  cantnflt  9697  cantnfp1lem3  9705  cantnflem3  9716  cnfcom  9725  cnfcom3lem  9728  ttrcltr  9741  rankssb  9873  tskwe  9975  dfac12lem2  10169  dfac12lem3  10170  cfflb  10284  cfcof  10299  ssfin2  10345  hsmexlem4  10454  ttukeylem6  10539  ttukeylem7  10540  fpwwe2lem1  10656  fpwwe2lem7  10662  fpwwe2lem10  10665  fpwwe2lem11  10666  canthnumlem  10673  canthwelem  10675  canthwe  10676  canthp1lem2  10678  pwfseqlem5  10688  wunex2  10763  tsktrss  10786  inttsk  10799  uzwo3  12960  supicc  13513  supiccub  13514  supicclub  13515  ssfzunsnext  13581  seqsplit  14036  seqf1olem2a  14041  seqz  14051  swrdval2  14632  trrelssd  14956  rtrclreclem4  15044  sumss  15706  qshash  15809  incexc  15819  incexc2  15820  prodss  15927  rpnnen2lem11  16204  vdwlem1  16953  ramub1lem1  16998  imasaddvallem  17514  imasvscaf  17524  mrerintcl  17580  ismred2  17586  mremre  17587  mrcuni  17604  mressmrcd  17610  submrc  17611  mrissmrid  17624  mreexexlem2d  17628  isacs2  17636  isacs1i  17640  invss  17747  ssctr  17811  funcres2b  17886  isacs3lem  18537  acsfiindd  18548  acsmapd  18549  acsmap2d  18550  tsrdir  18599  subsubmgm  18673  subsubm  18776  gsumwspan  18806  subsubg  19112  subgint  19113  cntzidss  19303  symggen  19437  pmtrdifellem1  19443  pmtrdifellem2  19444  pgpssslw  19581  lsmless1x  19611  lsmless2x  19612  lsmless12  19629  subglsm  19640  gsumval3lem2  19873  gsumzaddlem  19888  gsumzadd  19889  gsum2d  19939  dmdprdd  19968  dprdfeq0  19991  dprdspan  19996  dprdres  19997  dprdss  19998  dprdz  19999  subgdmdprd  20003  subgdprd  20004  dprdsn  20005  dprd2dlem1  20010  dprd2da  20011  dmdprdsplit2lem  20014  dprdsplit  20017  pgpfac1lem2  20044  pgpfac1lem3  20046  pgpfac1lem5  20048  subsubrng  20512  subsubrg  20549  subdrgint  20703  lspss  20880  lspun  20883  lsslsp  20911  lsslspOLD  20912  lmhmlsp  20946  lsmelval2  20982  lsmssspx  20985  lsppratlem2  21048  lsppratlem3  21049  lsppratlem4  21050  lbsextlem2  21059  lbsextlem3  21060  ocvlsp  21625  cssmre  21642  obselocv  21679  obslbs  21681  aspss  21827  mhpaddcl  22098  mhpinvcl  22099  mhpvscacl  22101  psdmullem  22112  toponmre  23041  neiint  23052  neiss  23057  lpss  23090  lpss3  23092  restopnb  23123  restfpw  23127  neitr  23128  restcls  23129  restntr  23130  restlp  23131  ordtbas  23140  pnfnei  23168  mnfnei  23169  iscnp4  23211  cnclsi  23220  isreg2  23325  discmp  23346  cmpcld  23350  uncmp  23351  sscmp  23353  hauscmplem  23354  cmpfi  23356  iunconnlem  23375  clsconn  23378  2ndcctbss  23403  restnlly  23430  llyrest  23433  nllyrest  23434  llyidm  23436  nllyidm  23437  cldllycmp  23443  dislly  23445  comppfsc  23480  llycmpkgen2  23498  ptbasfi  23529  txnlly  23585  txcmplem1  23589  tx1stc  23598  xkococnlem  23607  qtopval2  23644  basqtop  23659  tgqtop  23660  qtoprest  23665  kqreglem1  23689  kqreglem2  23690  kqnrmlem1  23691  kqnrmlem2  23692  fsubbas  23815  fgabs  23827  fbasrn  23832  trfil2  23835  trfg  23839  isufil2  23856  trufil  23858  ssufl  23866  ufileu  23867  filufint  23868  fmfnfmlem4  23905  fmfnfm  23906  flimss2  23920  flimss1  23921  fclsfnflim  23975  flimfnfcls  23976  fclscmp  23978  cnpfcfi  23988  alexsubALT  23999  clssubg  24057  clsnsg  24058  tsmsres  24092  ustexsym  24164  ustex2sym  24165  ustex3sym  24166  ustneism  24172  trust  24178  utoptop  24183  restutopopn  24187  utop2nei  24199  utopreg  24201  cfiluweak  24244  neipcfilu  24245  blssps  24374  blss  24375  blcld  24458  blsscls  24460  met1stc  24474  met2ndci  24475  metust  24511  cfilucfil  24512  restmetu  24523  tgqioo  24760  xrsblre  24771  reconnlem2  24787  xrge0gsumle  24793  xrge0tsms  24794  rescncf  24861  cnmpopc  24893  cnheibor  24925  cnllycmp  24926  lebnum  24934  phtpycn  24953  cfilfcls  25246  iscmet3lem2  25264  cmetss  25288  cncmet  25294  bcthlem4  25299  bcth3  25303  rrxcph  25364  rrxmetlem  25379  minveclem4a  25402  minveclem4  25404  ivthicc  25431  ovollb  25452  ovollb2lem  25461  ovollb2  25462  nulmbl2  25509  ioorcl2  25545  uniioombllem3  25558  uniioombllem4  25559  uniioombllem5  25560  opnmbllem  25574  volcn  25579  volivth  25580  mbfeqalem1  25614  itg10a  25684  mbfi1fseqlem4  25692  ditgcl  25831  ditgswap  25832  ditgsplitlem  25833  limcflf  25854  limcres  25859  dvbss  25874  dvbsss  25875  perfdvf  25876  dvreslem  25882  dvres2lem  25883  dvres3  25886  dvmptresicc  25889  dvcnp  25892  dvcnp2  25893  dvcnp2OLD  25894  dvcn  25895  dvnff  25897  dvn2bss  25904  dvnres  25905  cpnord  25909  dvaddbr  25912  dvmulbr  25913  dvmulbrOLD  25914  dvcobr  25921  dvcobrOLD  25922  dvnfre  25928  dvmptres2  25938  dvmptntr  25947  dvcnvlem  25952  dvcnv  25953  dvferm1lem  25960  dvferm2lem  25962  dvlip  25970  dvlipcn  25971  dvlip2  25972  c1liplem1  25973  dvgt0lem1  25979  lhop1lem  25990  lhop  25993  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcnvre  25996  dvfsumle  25998  dvfsumleOLD  25999  dvfsumge  26000  dvfsumabs  26001  ftc1lem1  26014  ftc1lem2  26015  ftc1a  26016  ftc1lem4  26018  ftc2ditglem  26024  itgsubstlem  26027  ig1peu  26154  ig1pdvds  26159  taylfvallem1  26336  tayl0  26341  taylply2  26347  taylply2OLD  26348  taylply  26349  dvtaylp  26350  dvntaylp  26351  dvntaylp0  26352  taylthlem1  26353  ulmdvlem1  26381  ulmdvlem3  26383  psercn  26408  pserdvlem2  26410  abelth  26423  xrlimcnp  26945  lgamucov  27015  wilthlem2  27046  sqff1o  27159  chtublem  27189  pntlemq  27579  pntlemf  27583  sssslt1  27774  sssslt2  27775  scutbdaybnd  27794  scutbdaybnd2  27795  cofss  27896  coiniss  27897  tglineintmo  28518  ttgcontlem1  28767  pthdlem1  29652  shintcli  31211  shub1  31264  mdslmd1lem1  32207  mdexchi  32217  chirredlem1  32272  mdsymlem5  32289  sumdmdii  32297  sumdmdlem2  32301  fnpreimac  32538  fsuppinisegfi  32549  xrsupssd  32611  xrge0infssd  32613  swrdrn3  32765  swrdf1  32766  swrdrndisj  32767  pwrssmgc  32816  xrge0tsmsd  32861  fldgenss  33102  fldgenssp  33104  linds2eq  33193  elrspunidl  33240  ssdifidllem  33268  ssdifidlprm  33270  mxidlprm  33282  ssmxidllem  33285  ssmxidl  33286  qsdrnglem2  33308  rprmdvdsprod  33346  resssra  33418  lsssra  33419  lbsdiflsp0  33455  dimkerim  33456  fedgmullem1  33458  fedgmullem2  33459  fedgmul  33460  smatrcl  33528  locfinreflem  33572  cmpcref  33582  zarclsun  33602  zarclsiin  33603  zarclssn  33605  zarcmplem  33613  pnfneige0  33683  esum2d  33843  insiga  33887  sssigagen2  33896  dynkin  33917  dya2iocnei  34033  omsmon  34049  carsgclctunlem1  34068  carsggect  34069  omsmeas  34074  ftc2re  34361  fdvneggt  34363  fdvnegge  34365  reprsuc  34378  reprss  34380  reprlt  34382  reprinfz1  34385  logdivsqrle  34413  hgt750lemb  34419  bnj906  34692  bnj1020  34727  bnj1137  34757  bnj1408  34798  bnj1452  34814  erdszelem7  34938  erdszelem8  34939  erdsze2lem1  34944  connpconn  34976  cvmliftmolem1  35022  cvmlift2lem1  35043  cvmlift2lem9  35052  cvmlift2lem10  35053  cvmlift3lem6  35065  cvmlift3lem7  35066  satfsschain  35105  ss2mcls  35309  neibastop2lem  35975  fnemeet2  35982  fnejoin1  35983  ontgval  36046  unbdqndv1  36114  opnmbllem0  37260  ftc1anclem7  37303  ftc1anclem8  37304  ftc1anc  37305  sstotbnd2  37378  heiborlem1  37415  heiborlem8  37422  intidl  37633  lsmsat  38610  lssats  38614  lpssat  38615  lssatle  38617  lssat  38618  lsatcvatlem  38651  paddss12  39422  paddasslem17  39439  pmodlem1  39449  pmod1i  39451  pmodl42N  39454  elpcliN  39496  pclfinN  39503  polcon3N  39520  polcon2N  39522  paddunN  39530  pclfinclN  39553  poml5N  39557  osumcllem1N  39559  osumcllem2N  39560  osumcllem3N  39561  pl42lem2N  39583  pl42lem4N  39585  cdlemn5pre  40803  dihord1  40821  dihord2a  40822  dihord2b  40823  dihord5b  40862  dochss  40968  dochdmj1  40993  djhsumss  41010  djhunssN  41012  dochexmidlem2  41064  lclkrslem1  41140  lclkrslem2  41141  lcfrlem2  41146  aks4d1p4  41682  aks4d1p5  41683  aks4d1p7  41686  aks4d1p8  41690  aks6d1c2  41733  sticksstones1  41749  prjcrv0  42192  elrfi  42256  ismrcd1  42260  istopclsd  42262  mrefg2  42269  aomclem2  42621  aomclem6  42625  hbtlem6  42695  hbt  42696  oege2  42878  cantnftermord  42891  omabs2  42903  tfsconcat0b  42917  naddgeoa  42966  naddwordnexlem0  42968  naddwordnexlem1  42969  dfno2  43000  mptrcllem  43185  dfrcl2  43246  relexp0a  43288  trclimalb2  43298  frege81d  43319  k0004ss2  43724  imo72b2lem0  43737  imo72b2lem2  43739  imo72b2  43744  uzwo4  44559  ssin0  44561  ixpssmapc  44579  ssinc  44593  ssdec  44594  supxrre3  44845  uzfissfz  44846  ssuzfz  44869  supminfxr  44984  inficc  45057  ressiocsup  45077  ressioosup  45078  ressiooinf  45080  limccog  45146  limclner  45177  limsupres  45231  limsupresuz2  45235  limsupequzlem  45248  limsupvaluz2  45264  supcnvlimsup  45266  limsupgtlem  45303  liminfresuz2  45313  cncfmptssg  45397  cncfuni  45412  icccncfext  45413  dvresntr  45444  dvbdfbdioolem1  45454  dvdmsscn  45462  dvnxpaek  45468  dvnprodlem2  45473  stoweidlem59  45585  fourierdlem20  45653  fourierdlem42  45675  fourierdlem48  45680  fourierdlem49  45681  fourierdlem52  45684  fourierdlem58  45690  fourierdlem64  45696  fourierdlem73  45705  fourierdlem76  45708  fourierdlem80  45712  fourierdlem84  45716  fourierdlem93  45725  fourierdlem103  45735  fourierdlem104  45736  fourierdlem113  45745  etransclem18  45778  ioorrnopnlem  45830  salincl  45850  intsal  45856  fsumlesge0  45903  sge0cl  45907  sge0supre  45915  sge0less  45918  sge0split  45935  sge0seq  45972  caragensspw  46035  omessre  46036  caragendifcl  46040  caratheodorylem1  46052  0ome  46055  omess0  46060  caragencmpl  46061  hoicvr  46074  hoissrrn  46075  hoicvrrex  46082  ovnlecvr  46084  ovnsslelem  46086  ovnssle  46087  ovnsubaddlem1  46096  hoissrrn2  46104  hoidmv1lelem1  46117  hoidmvlelem1  46121  hoidmvlelem2  46122  hoidmvlelem4  46124  ovnlecvr2  46136  voncmpl  46147  hspmbl  46155  opnvonmbllem1  46158  ovolval5lem2  46179  ovolval5lem3  46180  vonioolem1  46206  pimdecfgtioc  46241  pimincfltioc  46242  pimdecfgtioo  46243  pimincfltioo  46244  issmflem  46253  cnfsmf  46266  incsmflem  46267  smfsssmf  46269  smfadd  46291  decsmflem  46292  smflim  46303  smfres  46316  smfmul  46321  smfpimbor1lem1  46324  smfco  46328  smfsuplem1  46337  smfsuplem3  46339  smflimsuplem1  46346  smflimsuplem4  46349  smflimsuplem7  46352  cnneiima  48121  seposep  48130  iscnrm3rlem4  48148  iscnrm3llem1  48154  lubsscl  48165  glbsscl  48166  toplatglb  48198  setrecsss  48318  elpglem1  48328