Theorem sstrd 3977

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

Syntax hints:   → wi 4   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  sstrid  3978  sstrdi  3979  rabssrabd  4058  ssdif2d  4120  uniintsn  4913  funss  6374  fssxp  6534  knatar  7110  tfisi  7573  suppssov1  7862  suppssfv  7866  tposss  7893  tfrlem1  8012  omwordri  8198  oewordri  8218  oeeui  8228  oaabs2  8272  omopthlem1  8282  ecinxp  8372  sbthlem1  8627  dffi2  8887  hartogslem1  9006  cantnfcl  9130  cantnflt  9135  cantnfp1lem3  9143  cantnflem3  9154  cnfcom  9163  cnfcom3lem  9166  rankssb  9277  tskwe  9379  dfac12lem2  9570  dfac12lem3  9571  cfflb  9681  cfcof  9696  ssfin2  9742  hsmexlem4  9851  ttukeylem6  9936  ttukeylem7  9937  fpwwe2lem1  10053  fpwwe2lem8  10059  fpwwe2lem11  10062  fpwwe2lem12  10063  canthnumlem  10070  canthwelem  10072  canthwe  10073  canthp1lem2  10075  pwfseqlem5  10085  wunex2  10160  tsktrss  10183  inttsk  10196  uzwo3  12344  supicc  12887  supiccub  12888  supicclub  12889  ssfzunsnext  12953  seqsplit  13404  seqf1olem2a  13409  seqz  13419  swrdval2  14008  trrelssd  14333  rtrclreclem4  14420  sumss  15081  qshash  15182  incexc  15192  incexc2  15193  prodss  15301  rpnnen2lem11  15577  vdwlem1  16317  ramub1lem1  16362  imasaddvallem  16802  imasvscaf  16812  mrerintcl  16868  ismred2  16874  mremre  16875  mrcuni  16892  mressmrcd  16898  submrc  16899  mrissmrid  16912  mreexexlem2d  16916  isacs2  16924  isacs1i  16928  invss  17031  ssctr  17095  funcres2b  17167  isacs3lem  17776  acsfiindd  17787  acsmapd  17788  acsmap2d  17789  tsrdir  17848  subsubm  17981  gsumwspan  18011  subsubg  18302  subgint  18303  cntzidss  18468  symggen  18598  pmtrdifellem1  18604  pmtrdifellem2  18605  pgpssslw  18739  lsmless1x  18769  lsmless2x  18770  lsmless12  18787  subglsm  18799  gsumval3lem2  19026  gsumzaddlem  19041  gsumzadd  19042  gsum2d  19092  dmdprdd  19121  dprdfeq0  19144  dprdspan  19149  dprdres  19150  dprdss  19151  dprdz  19152  subgdmdprd  19156  subgdprd  19157  dprdsn  19158  dprd2dlem1  19163  dprd2da  19164  dmdprdsplit2lem  19167  dprdsplit  19170  pgpfac1lem2  19197  pgpfac1lem3  19199  pgpfac1lem5  19201  subsubrg  19561  subdrgint  19582  lspss  19756  lspun  19759  lsslsp  19787  lmhmlsp  19821  lsmelval2  19857  lsmssspx  19860  lsppratlem2  19920  lsppratlem3  19921  lsppratlem4  19922  lbsextlem2  19931  lbsextlem3  19932  aspss  20106  mhpaddcl  20338  mhpvscacl  20341  ocvlsp  20820  cssmre  20837  obselocv  20872  obslbs  20874  toponmre  21701  neiint  21712  neiss  21717  lpss  21750  lpss3  21752  restopnb  21783  restfpw  21787  neitr  21788  restcls  21789  restntr  21790  restlp  21791  ordtbas  21800  pnfnei  21828  mnfnei  21829  iscnp4  21871  cnclsi  21880  isreg2  21985  discmp  22006  cmpcld  22010  uncmp  22011  sscmp  22013  hauscmplem  22014  cmpfi  22016  iunconnlem  22035  clsconn  22038  2ndcctbss  22063  restnlly  22090  llyrest  22093  nllyrest  22094  llyidm  22096  nllyidm  22097  cldllycmp  22103  dislly  22105  comppfsc  22140  llycmpkgen2  22158  ptbasfi  22189  txnlly  22245  txcmplem1  22249  tx1stc  22258  xkococnlem  22267  qtopval2  22304  basqtop  22319  tgqtop  22320  qtoprest  22325  kqreglem1  22349  kqreglem2  22350  kqnrmlem1  22351  kqnrmlem2  22352  fsubbas  22475  fgabs  22487  fbasrn  22492  trfil2  22495  trfg  22499  isufil2  22516  trufil  22518  ssufl  22526  ufileu  22527  filufint  22528  fmfnfmlem4  22565  fmfnfm  22566  flimss2  22580  flimss1  22581  fclsfnflim  22635  flimfnfcls  22636  fclscmp  22638  cnpfcfi  22648  alexsubALT  22659  clssubg  22717  clsnsg  22718  tsmsres  22752  ustexsym  22824  ustex2sym  22825  ustex3sym  22826  ustneism  22832  trust  22838  utoptop  22843  restutopopn  22847  utop2nei  22859  utopreg  22861  cfiluweak  22904  neipcfilu  22905  blssps  23034  blss  23035  blcld  23115  blsscls  23117  met1stc  23131  met2ndci  23132  metust  23168  cfilucfil  23169  restmetu  23180  tgqioo  23408  xrsblre  23419  reconnlem2  23435  xrge0gsumle  23441  xrge0tsms  23442  rescncf  23505  cnmpopc  23532  cnheibor  23559  cnllycmp  23560  lebnum  23568  phtpycn  23587  cfilfcls  23877  iscmet3lem2  23895  cmetss  23919  cncmet  23925  bcthlem4  23930  bcth3  23934  rrxcph  23995  rrxmetlem  24010  minveclem4a  24033  minveclem4  24035  ivthicc  24059  ovollb  24080  ovollb2lem  24089  ovollb2  24090  nulmbl2  24137  ioorcl2  24173  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  opnmbllem  24202  volcn  24207  volivth  24208  mbfeqalem1  24242  itg10a  24311  mbfi1fseqlem4  24319  ditgcl  24456  ditgswap  24457  ditgsplitlem  24458  limcflf  24479  limcres  24484  dvbss  24499  dvbsss  24500  perfdvf  24501  dvreslem  24507  dvres2lem  24508  dvres3  24511  dvcnp  24516  dvcnp2  24517  dvcn  24518  dvnff  24520  dvn2bss  24527  dvnres  24528  cpnord  24532  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvnfre  24549  dvmptres2  24559  dvmptntr  24568  dvcnvlem  24573  dvcnv  24574  dvferm1lem  24581  dvferm2lem  24583  dvlip  24590  dvlipcn  24591  dvlip2  24592  c1liplem1  24593  dvgt0lem1  24599  lhop1lem  24610  lhop  24613  dvcnvrelem1  24614  dvcnvrelem2  24615  dvcnvre  24616  dvfsumle  24618  dvfsumge  24619  dvfsumabs  24620  ftc1lem1  24632  ftc1lem2  24633  ftc1a  24634  ftc1lem4  24636  ftc2ditglem  24642  itgsubstlem  24645  ig1peu  24765  ig1pdvds  24770  taylfvallem1  24945  tayl0  24950  taylply2  24956  taylply  24957  dvtaylp  24958  dvntaylp  24959  dvntaylp0  24960  taylthlem1  24961  ulmdvlem1  24988  ulmdvlem3  24990  psercn  25014  pserdvlem2  25016  abelth  25029  xrlimcnp  25546  lgamucov  25615  wilthlem2  25646  sqff1o  25759  chtublem  25787  pntlemq  26177  pntlemf  26181  tglineintmo  26428  ttgcontlem1  26671  pthdlem1  27547  shintcli  29106  shub1  29159  mdslmd1lem1  30102  mdexchi  30112  chirredlem1  30167  mdsymlem5  30184  sumdmdii  30192  sumdmdlem2  30196  fnpreimac  30416  xrsupssd  30483  xrge0infssd  30485  swrdrn3  30629  swrdf1  30630  swrdrndisj  30631  xrge0tsmsd  30692  linds2eq  30941  mxidlprm  30977  ssmxidllem  30978  ssmxidl  30979  lbsdiflsp0  31022  dimkerim  31023  fedgmullem1  31025  fedgmullem2  31026  fedgmul  31027  smatrcl  31061  locfinreflem  31104  cmpcref  31114  pnfneige0  31194  esum2d  31352  insiga  31396  sssigagen2  31405  dynkin  31426  dya2iocnei  31540  omsmon  31556  carsgclctunlem1  31575  carsggect  31576  omsmeas  31581  ftc2re  31869  fdvneggt  31871  fdvnegge  31873  reprsuc  31886  reprss  31888  reprlt  31890  reprinfz1  31893  logdivsqrle  31921  hgt750lemb  31927  bnj906  32202  bnj1020  32237  bnj1137  32267  bnj1408  32308  bnj1452  32324  erdszelem7  32444  erdszelem8  32445  erdsze2lem1  32450  connpconn  32482  cvmliftmolem1  32528  cvmlift2lem1  32549  cvmlift2lem9  32558  cvmlift2lem10  32559  cvmlift3lem6  32571  cvmlift3lem7  32572  satfsschain  32611  ss2mcls  32815  dftrpred3g  33072  frrlem8  33130  sssslt1  33260  sssslt2  33261  scutbdaybnd  33275  neibastop2lem  33708  fnemeet2  33715  fnejoin1  33716  ontgval  33779  unbdqndv1  33847  opnmbllem0  34943  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  sstotbnd2  35067  heiborlem1  35104  heiborlem8  35111  intidl  35322  lsmsat  36159  lssats  36163  lpssat  36164  lssatle  36166  lssat  36167  lsatcvatlem  36200  paddss12  36970  paddasslem17  36987  pmodlem1  36997  pmod1i  36999  pmodl42N  37002  elpcliN  37044  pclfinN  37051  polcon3N  37068  polcon2N  37070  paddunN  37078  pclfinclN  37101  poml5N  37105  osumcllem1N  37107  osumcllem2N  37108  osumcllem3N  37109  pl42lem2N  37131  pl42lem4N  37133  cdlemn5pre  38351  dihord1  38369  dihord2a  38370  dihord2b  38371  dihord5b  38410  dochss  38516  dochdmj1  38541  djhsumss  38558  djhunssN  38560  dochexmidlem2  38612  lclkrslem1  38688  lclkrslem2  38689  lcfrlem2  38694  elrfi  39340  ismrcd1  39344  istopclsd  39346  mrefg2  39353  aomclem2  39704  aomclem6  39708  hbtlem6  39778  hbt  39779  mptrcllem  40022  dfrcl2  40068  relexp0a  40110  trclimalb2  40120  frege81d  40141  k0004ss2  40551  imo72b2lem0  40565  imo72b2lem2  40567  imo72b2  40574  uzwo4  41364  ssin0  41366  ixpssmapc  41385  ssinc  41402  ssdec  41403  supxrre3  41642  uzfissfz  41643  ssuzfz  41666  supminfxr  41789  inficc  41859  ressiocsup  41879  ressioosup  41880  ressiooinf  41882  limccog  41950  limclner  41981  limsupres  42035  limsupresuz2  42039  limsupequzlem  42052  limsupvaluz2  42068  supcnvlimsup  42070  limsupgtlem  42107  liminfresuz2  42117  cncfmptssg  42202  cncfuni  42218  icccncfext  42219  dvresntr  42251  dvmptresicc  42253  dvbdfbdioolem1  42262  dvdmsscn  42270  dvnxpaek  42276  dvnprodlem2  42281  stoweidlem59  42393  fourierdlem20  42461  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem52  42492  fourierdlem58  42498  fourierdlem64  42504  fourierdlem73  42513  fourierdlem76  42516  fourierdlem80  42520  fourierdlem84  42524  fourierdlem93  42533  fourierdlem103  42543  fourierdlem104  42544  fourierdlem113  42553  etransclem18  42586  ioorrnopnlem  42638  salincl  42657  intsal  42662  fsumlesge0  42708  sge0cl  42712  sge0supre  42720  sge0less  42723  sge0split  42740  sge0seq  42777  caragensspw  42840  omessre  42841  caragendifcl  42845  caratheodorylem1  42857  0ome  42860  omess0  42865  caragencmpl  42866  hoicvr  42879  hoissrrn  42880  hoicvrrex  42887  ovnlecvr  42889  ovnsslelem  42891  ovnssle  42892  ovnsubaddlem1  42901  hoissrrn2  42909  hoidmv1lelem1  42922  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem4  42929  ovnlecvr2  42941  voncmpl  42952  hspmbl  42960  opnvonmbllem1  42963  ovolval5lem2  42984  ovolval5lem3  42985  vonioolem1  43011  pimdecfgtioc  43042  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  issmflem  43053  cnfsmf  43066  incsmflem  43067  smfsssmf  43069  smfadd  43090  decsmflem  43091  smflim  43102  smfres  43114  smfmul  43119  smfpimbor1lem1  43122  smfco  43126  smfsuplem1  43134  smfsuplem3  43136  smflimsuplem1  43143  smflimsuplem4  43146  smflimsuplem7  43149  subsubmgm  44113  setrecsss  44852  elpglem1  44862