Theorem sstrd 3808

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

Syntax hints:   → wi 4   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783

This theorem is referenced by:  syl5ss  3809  syl6ss  3810  rabssrabd  3886  ssdif2d  3948  uniintsn  4706  funss  6116  fssxp  6271  fimass  6292  knatar  6827  tfisi  7284  suppfnssOLD  7551  suppssov1  7558  suppssfv  7562  tposss  7584  tfrlem1  7704  omwordri  7885  oewordri  7905  oeeui  7915  oaabs2  7958  omopthlem1  7968  ecinxp  8053  sbthlem1  8305  dffi2  8564  hartogslem1  8682  cantnfcl  8807  cantnflt  8812  cantnfp1lem3  8820  cantnflem3  8831  cnfcom  8840  cnfcom3lem  8843  rankssb  8954  tskwe  9055  dfac12lem2  9247  dfac12lem3  9248  cfflb  9362  cfcof  9377  ssfin2  9423  hsmexlem4  9532  ttukeylem6  9617  ttukeylem7  9618  fpwwe2lem1  9734  fpwwe2lem8  9740  fpwwe2lem11  9743  fpwwe2lem12  9744  canthnumlem  9751  canthwelem  9753  canthwe  9754  canthp1lem2  9756  pwfseqlem5  9766  wunex2  9841  tsktrss  9864  inttsk  9877  uzwo3  11998  supicc  12539  supiccub  12540  supicclub  12541  ssfzunsnext  12605  seqsplit  13053  seqf1olem2a  13058  seqz  13068  swrdval2  13639  trrelssd  13933  rtrclreclem4  14020  sumss  14674  qshash  14777  incexc  14787  incexc2  14788  prodss  14894  rpnnen2lem11  15169  vdwlem1  15898  ramub1lem1  15943  imasaddvallem  16390  imasvscaf  16400  mrerintcl  16458  ismred2  16464  mremre  16465  mrcuni  16482  mressmrcd  16488  submrc  16489  mrissmrid  16502  mreexexlem2d  16506  isacs2  16514  isacs1i  16518  invss  16621  ssctr  16685  funcres2b  16757  isacs3lem  17367  acsfiindd  17378  acsmapd  17379  acsmap2d  17380  tsrdir  17439  subsubm  17558  gsumwspan  17584  subsubg  17815  subgint  17816  cntzidss  17967  symggen  18087  pmtrdifellem1  18093  pmtrdifellem2  18094  pgpssslw  18226  lsmless1x  18256  lsmless2x  18257  lsmless12  18273  subglsm  18283  gsumval3lem2  18504  gsumzaddlem  18518  gsumzadd  18519  gsum2d  18568  dmdprdd  18596  dprdfeq0  18619  dprdspan  18624  dprdres  18625  dprdss  18626  dprdz  18627  subgdmdprd  18631  subgdprd  18632  dprdsn  18633  dprd2dlem1  18638  dprd2da  18639  dmdprdsplit2lem  18642  dprdsplit  18645  pgpfac1lem2  18672  pgpfac1lem3  18674  pgpfac1lem5  18676  subsubrg  19006  lspss  19187  lspun  19190  lsslsp  19218  lmhmlsp  19252  lsmelval2  19288  lsmssspx  19291  lsppratlem2  19353  lsppratlem3  19354  lsppratlem4  19355  lbsextlem2  19364  lbsextlem3  19365  aspss  19537  ocvlsp  20227  cssmre  20244  obselocv  20279  obslbs  20281  toponmre  21108  neiint  21119  neiss  21124  lpss  21157  lpss3  21159  restopnb  21190  restfpw  21194  neitr  21195  restcls  21196  restntr  21197  restlp  21198  ordtbas  21207  pnfnei  21235  mnfnei  21236  iscnp4  21278  cnclsi  21287  isreg2  21392  discmp  21412  cmpcld  21416  uncmp  21417  sscmp  21419  hauscmplem  21420  cmpfi  21422  iunconnlem  21441  clsconn  21444  2ndcctbss  21469  restnlly  21496  llyrest  21499  nllyrest  21500  llyidm  21502  nllyidm  21503  cldllycmp  21509  dislly  21511  comppfsc  21546  llycmpkgen2  21564  ptbasfi  21595  txnlly  21651  txcmplem1  21655  tx1stc  21664  xkococnlem  21673  qtopval2  21710  basqtop  21725  tgqtop  21726  qtoprest  21731  kqreglem1  21755  kqreglem2  21756  kqnrmlem1  21757  kqnrmlem2  21758  fsubbas  21881  fgabs  21893  fbasrn  21898  trfil2  21901  trfg  21905  isufil2  21922  trufil  21924  ssufl  21932  ufileu  21933  filufint  21934  fmfnfmlem4  21971  fmfnfm  21972  flimss2  21986  flimss1  21987  fclsfnflim  22041  flimfnfcls  22042  fclscmp  22044  cnpfcfi  22054  alexsubALT  22065  clssubg  22122  clsnsg  22123  tsmsres  22157  ustexsym  22229  ustex2sym  22230  ustex3sym  22231  ustund  22235  ustneism  22237  trust  22243  utoptop  22248  restutopopn  22252  utop2nei  22264  utopreg  22266  cfiluweak  22309  neipcfilu  22310  blssps  22439  blss  22440  blcld  22520  blsscls  22522  met1stc  22536  met2ndci  22537  metust  22573  cfilucfil  22574  restmetu  22585  tgqioo  22813  xrsblre  22824  reconnlem2  22840  xrge0gsumle  22846  xrge0tsms  22847  rescncf  22910  cnmpt2pc  22937  cnheibor  22964  cnllycmp  22965  lebnum  22973  phtpycn  22992  cfilfcls  23282  iscmet3lem2  23300  cmetss  23323  cncmet  23329  bcthlem4  23334  bcth3  23338  rrxcph  23391  rrxmetlem  23401  minveclem4a  23412  minveclem4  23414  ivthicc  23438  ovollb  23459  ovollb2lem  23468  ovollb2  23469  nulmbl2  23516  ioorcl2  23552  uniioombllem3  23565  uniioombllem4  23566  uniioombllem5  23567  opnmbllem  23581  volcn  23586  volivth  23587  mbfeqalem1  23621  itg10a  23690  mbfi1fseqlem4  23698  ditgcl  23835  ditgswap  23836  ditgsplitlem  23837  limcflf  23858  limcres  23863  dvbss  23878  dvbsss  23879  perfdvf  23880  dvreslem  23886  dvres2lem  23887  dvres3  23890  dvcnp  23895  dvcnp2  23896  dvcn  23897  dvnff  23899  dvn2bss  23906  dvnres  23907  cpnord  23911  dvaddbr  23914  dvmulbr  23915  dvcobr  23922  dvnfre  23928  dvmptres2  23938  dvmptntr  23947  dvcnvlem  23952  dvcnv  23953  dvferm1lem  23960  dvferm2lem  23962  dvlip  23969  dvlipcn  23970  dvlip2  23971  c1liplem1  23972  dvgt0lem1  23978  lhop1lem  23989  lhop  23992  dvcnvrelem1  23993  dvcnvrelem2  23994  dvcnvre  23995  dvfsumle  23997  dvfsumge  23998  dvfsumabs  23999  ftc1lem1  24011  ftc1lem2  24012  ftc1a  24013  ftc1lem4  24015  ftc2ditglem  24021  itgsubstlem  24024  ig1peu  24144  ig1pdvds  24149  taylfvallem1  24324  tayl0  24329  taylply2  24335  taylply  24336  dvtaylp  24337  dvntaylp  24338  dvntaylp0  24339  taylthlem1  24340  ulmdvlem1  24367  ulmdvlem3  24369  psercn  24393  pserdvlem2  24395  abelth  24408  xrlimcnp  24908  lgamucov  24977  wilthlem2  25008  sqff1o  25121  chtublem  25149  pntlemq  25503  pntlemf  25507  tglineintmo  25750  ttgcontlem1  25978  pthdlem1  26889  shintcli  28515  shub1  28568  mdslmd1lem1  29511  mdexchi  29521  chirredlem1  29576  mdsymlem5  29593  sumdmdii  29601  sumdmdlem2  29605  xrsupssd  29850  xrge0infssd  29852  xrge0tsmsd  30109  smatrcl  30186  locfinreflem  30231  cmpcref  30241  pnfneige0  30321  esum2d  30479  insiga  30524  sssigagen2  30533  dynkin  30554  dya2iocnei  30668  omsmon  30684  carsgclctunlem1  30703  carsggect  30704  omsmeas  30709  ftc2re  31000  fdvneggt  31002  fdvnegge  31004  reprsuc  31017  reprss  31019  reprlt  31021  reprinfz1  31024  logdivsqrle  31052  hgt750lemb  31058  bnj906  31321  bnj1020  31354  bnj1137  31384  bnj1408  31425  bnj1452  31441  erdszelem7  31500  erdszelem8  31501  erdsze2lem1  31506  connpconn  31538  cvmliftmolem1  31584  cvmlift2lem1  31605  cvmlift2lem9  31614  cvmlift2lem10  31615  cvmlift3lem6  31627  cvmlift3lem7  31628  ss2mcls  31786  dftrpred3g  32051  sssslt1  32225  sssslt2  32226  scutbdaybnd  32240  neibastop2lem  32674  fnemeet2  32681  fnejoin1  32682  ontgval  32745  unbdqndv1  32814  opnmbllem0  33756  ftc1anclem7  33801  ftc1anclem8  33802  ftc1anc  33803  sstotbnd2  33882  heiborlem1  33919  heiborlem8  33926  intidl  34137  lsmsat  34786  lssats  34790  lpssat  34791  lssatle  34793  lssat  34794  lsatcvatlem  34827  paddss12  35597  paddasslem17  35614  pmodlem1  35624  pmod1i  35626  pmodl42N  35629  elpcliN  35671  pclfinN  35678  polcon3N  35695  polcon2N  35697  paddunN  35705  pclfinclN  35728  poml5N  35732  osumcllem1N  35734  osumcllem2N  35735  osumcllem3N  35736  pl42lem2N  35758  pl42lem4N  35760  cdlemn5pre  36978  dihord1  36996  dihord2a  36997  dihord2b  36998  dihord5b  37037  dochss  37143  dochdmj1  37168  djhsumss  37185  djhunssN  37187  dochexmidlem2  37239  lclkrslem1  37315  lclkrslem2  37316  lcfrlem2  37321  elrfi  37756  ismrcd1  37760  istopclsd  37762  mrefg2  37769  aomclem2  38123  aomclem6  38127  hbtlem6  38197  hbt  38198  mptrcllem  38417  dfrcl2  38463  relexp0a  38505  trclimalb2  38515  frege81d  38536  k0004ss2  38947  imo72b2lem0  38962  imo72b2lem2  38964  imo72b2lem1  38968  imo72b2  38972  uzwo4  39711  ssin0  39713  ixpssmapc  39733  ssinc  39754  ssdec  39755  supxrre3  40018  uzfissfz  40019  ssuzfz  40042  ssrexr  40135  supminfxr  40170  inficc  40238  ressiocsup  40258  ressioosup  40259  ressiooinf  40261  limccog  40329  limclner  40360  limsuppnfdlem  40410  limsupres  40414  limsupresuz2  40418  limsupequzlem  40431  limsupvaluz2  40447  supcnvlimsup  40449  limsupgtlem  40486  liminfresuz2  40496  cncfmptssg  40560  cncfuni  40576  icccncfext  40577  dvresntr  40609  dvmptresicc  40611  dvbdfbdioolem1  40620  dvdmsscn  40628  dvnxpaek  40634  dvnprodlem2  40639  stoweidlem59  40752  fourierdlem20  40820  fourierdlem42  40842  fourierdlem48  40847  fourierdlem49  40848  fourierdlem52  40851  fourierdlem58  40857  fourierdlem64  40863  fourierdlem73  40872  fourierdlem76  40875  fourierdlem80  40879  fourierdlem84  40883  fourierdlem93  40892  fourierdlem103  40902  fourierdlem104  40903  fourierdlem113  40912  etransclem18  40945  ioorrnopnlem  41000  salincl  41019  intsal  41024  fsumlesge0  41070  sge0cl  41074  sge0supre  41082  sge0less  41085  sge0split  41102  sge0seq  41139  caragensspw  41202  omessre  41203  caragendifcl  41207  caratheodorylem1  41219  0ome  41222  omess0  41227  caragencmpl  41228  hoicvr  41241  hoissrrn  41242  hoicvrrex  41249  ovnlecvr  41251  ovnsslelem  41253  ovnssle  41254  ovnsubaddlem1  41263  hoissrrn2  41271  hoidmv1lelem1  41284  hoidmvlelem1  41288  hoidmvlelem2  41289  hoidmvlelem4  41291  ovnlecvr2  41303  voncmpl  41314  hspmbl  41322  opnvonmbllem1  41325  ovolval5lem2  41346  ovolval5lem3  41347  vonioolem1  41373  pimdecfgtioc  41404  pimincfltioc  41405  pimdecfgtioo  41406  pimincfltioo  41407  issmflem  41415  cnfsmf  41428  incsmflem  41429  smfsssmf  41431  smfadd  41452  decsmflem  41453  smflim  41464  smfres  41476  smfmul  41481  smfpimbor1lem1  41484  smfco  41488  smfsuplem1  41496  smfsuplem3  41498  smflimsuplem1  41505  smflimsuplem4  41508  smflimsuplem7  41511  subsubmgm  42362  setrecsss  43012  elpglem1  43022