Theorem sstrd 3578

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

Syntax hints:   → wi 4   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  syl5ss  3579  syl6ss  3580  ssdif2d  3711  uniintsn  4449  funss  5822  fssxp  5973  fimass  5994  knatar  6507  tfisi  6950  suppfnss  7207  suppssov1  7214  suppssfv  7218  tposss  7240  tfrlem1  7359  omwordri  7539  oewordri  7559  oeeui  7569  oaabs2  7612  omopthlem1  7622  ecinxp  7709  sbthlem1  7955  dffi2  8212  hartogslem1  8330  cantnfcl  8447  cantnflt  8452  cantnfp1lem3  8460  cantnflem3  8471  cnfcom  8480  cnfcom3lem  8483  rankssb  8594  tskwe  8659  dfac12lem2  8849  dfac12lem3  8850  cfflb  8964  cfcof  8979  ssfin2  9025  hsmexlem4  9134  ttukeylem6  9219  ttukeylem7  9220  fpwwe2lem1  9332  fpwwe2lem8  9338  fpwwe2lem11  9341  fpwwe2lem12  9342  canthnumlem  9349  canthwelem  9351  canthwe  9352  canthp1lem2  9354  pwfseqlem5  9364  wunex2  9439  tsktrss  9462  inttsk  9475  uzwo3  11659  supicc  12191  supiccub  12192  supicclub  12193  ssfzunsn  12257  seqsplit  12696  seqf1olem2a  12701  seqz  12711  swrdval2  13272  trrelssd  13560  rtrclreclem4  13649  sumss  14302  qshash  14398  incexc  14408  incexc2  14409  prodss  14516  rpnnen2lem11  14792  vdwlem1  15523  ramub1lem1  15568  imasaddvallem  16012  imasvscaf  16022  mrerintcl  16080  ismred2  16086  mremre  16087  mrcuni  16104  mressmrcd  16110  submrc  16111  mrissmrid  16124  mreexexlem2d  16128  isacs2  16137  isacs1i  16141  invss  16244  ssctr  16308  funcres2b  16380  isacs3lem  16989  acsfiindd  17000  acsmapd  17001  acsmap2d  17002  tsrdir  17061  subsubm  17180  gsumwspan  17206  subsubg  17440  subgint  17441  cntzidss  17593  symggen  17713  pmtrdifellem1  17719  pmtrdifellem2  17720  pgpssslw  17852  lsmless1x  17882  lsmless2x  17883  lsmless12  17899  subglsm  17909  gsumval3lem2  18130  gsumzaddlem  18144  gsumzadd  18145  gsum2d  18194  dmdprdd  18221  dprdfeq0  18244  dprdspan  18249  dprdres  18250  dprdss  18251  dprdz  18252  subgdmdprd  18256  subgdprd  18257  dprdsn  18258  dprd2dlem1  18263  dprd2da  18264  dmdprdsplit2lem  18267  dprdsplit  18270  pgpfac1lem2  18297  pgpfac1lem3  18299  pgpfac1lem5  18301  subsubrg  18629  lspss  18805  lspun  18808  lsslsp  18836  lmhmlsp  18870  lsmelval2  18906  lsmssspx  18909  lsppratlem2  18969  lsppratlem3  18970  lsppratlem4  18971  lbsextlem2  18980  lbsextlem3  18981  aspss  19153  ocvlsp  19839  cssmre  19856  obselocv  19891  obslbs  19893  toponmre  20707  neiint  20718  neiss  20723  lpss  20756  lpss3  20758  restopnb  20789  restfpw  20793  neitr  20794  restcls  20795  restntr  20796  restlp  20797  ordtbas  20806  pnfnei  20834  mnfnei  20835  iscnp4  20877  cnclsi  20886  isreg2  20991  discmp  21011  cmpcld  21015  uncmp  21016  sscmp  21018  hauscmplem  21019  cmpfi  21021  iunconlem  21040  clscon  21043  2ndcctbss  21068  restnlly  21095  llyrest  21098  nllyrest  21099  llyidm  21101  nllyidm  21102  cldllycmp  21108  dislly  21110  comppfsc  21145  llycmpkgen2  21163  ptbasfi  21194  txnlly  21250  txcmplem1  21254  tx1stc  21263  xkococnlem  21272  qtopval2  21309  basqtop  21324  tgqtop  21325  qtoprest  21330  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  fsubbas  21481  fgabs  21493  fbasrn  21498  trfil2  21501  trfg  21505  isufil2  21522  trufil  21524  ssufl  21532  ufileu  21533  filufint  21534  fmfnfmlem4  21571  fmfnfm  21572  flimss2  21586  flimss1  21587  fclsfnflim  21641  flimfnfcls  21642  fclscmp  21644  cnpfcfi  21654  alexsubALT  21665  clssubg  21722  clsnsg  21723  tsmsres  21757  ustexsym  21829  ustex2sym  21830  ustex3sym  21831  ustund  21835  ustneism  21837  trust  21843  utoptop  21848  restutopopn  21852  utop2nei  21864  utopreg  21866  cfiluweak  21909  neipcfilu  21910  blssps  22039  blss  22040  blcld  22120  blsscls  22122  met1stc  22136  met2ndci  22137  metust  22173  cfilucfil  22174  restmetu  22185  tgqioo  22411  xrsblre  22422  reconnlem2  22438  xrge0gsumle  22444  xrge0tsms  22445  rescncf  22508  cnmpt2pc  22535  cnheibor  22562  cnllycmp  22563  lebnum  22571  phtpycn  22590  cfilfcls  22880  iscmet3lem2  22898  cmetss  22921  cncmet  22927  bcthlem4  22932  bcth3  22936  rrxcph  22988  rrxmetlem  22998  minveclem4a  23009  minveclem4  23011  ivthicc  23034  ovollb  23054  ovollb2lem  23063  ovollb2  23064  nulmbl2  23111  ioorcl2  23146  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  opnmbllem  23175  volcn  23180  volivth  23181  mbfeqalem  23215  itg10a  23283  mbfi1fseqlem4  23291  ditgcl  23428  ditgswap  23429  ditgsplitlem  23430  limcflf  23451  limcres  23456  dvbss  23471  dvbsss  23472  perfdvf  23473  dvreslem  23479  dvres2lem  23480  dvres3  23483  dvcnp  23488  dvcnp2  23489  dvcn  23490  dvnff  23492  dvn2bss  23499  dvnres  23500  cpnord  23504  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvnfre  23521  dvmptres2  23531  dvmptntr  23540  dvcnvlem  23543  dvcnv  23544  dvferm1lem  23551  dvferm2lem  23553  dvlip  23560  dvlipcn  23561  dvlip2  23562  c1liplem1  23563  dvgt0lem1  23569  lhop1lem  23580  lhop  23583  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcnvre  23586  dvfsumle  23588  dvfsumge  23589  dvfsumabs  23590  ftc1lem1  23602  ftc1lem2  23603  ftc1a  23604  ftc1lem4  23606  ftc2ditglem  23612  itgsubstlem  23615  ig1peu  23735  ig1pdvds  23740  taylfvallem1  23915  tayl0  23920  taylply2  23926  taylply  23927  dvtaylp  23928  dvntaylp  23929  dvntaylp0  23930  taylthlem1  23931  ulmdvlem1  23958  ulmdvlem3  23960  psercn  23984  pserdvlem2  23986  abelth  23999  xrlimcnp  24495  lgamucov  24564  wilthlem2  24595  sqff1o  24708  chtublem  24736  pntlemq  25090  pntlemf  25094  tglineintmo  25337  ttgcontlem1  25565  shintcli  27572  shub1  27625  mdslmd1lem1  28568  mdexchi  28578  chirredlem1  28633  mdsymlem5  28650  sumdmdii  28658  sumdmdlem2  28662  xrsupssd  28914  xrge0infssd  28916  xrge0tsmsd  29116  smatrcl  29190  locfinreflem  29235  cmpcref  29245  pnfneige0  29325  esum2d  29482  insiga  29527  sssigagen2  29536  dynkin  29557  dya2iocnei  29671  omsmon  29687  carsgclctunlem1  29706  carsggect  29707  omsmeas  29712  bnj906  30254  bnj1020  30287  bnj1137  30317  bnj1408  30358  bnj1452  30374  erdszelem7  30433  erdszelem8  30434  erdsze2lem1  30439  conpcon  30471  cvmliftmolem1  30517  cvmlift2lem1  30538  cvmlift2lem9  30547  cvmlift2lem10  30548  cvmlift3lem6  30560  cvmlift3lem7  30561  ss2mcls  30719  dftrpred3g  30977  nofulllem3  31103  neibastop2lem  31525  fnemeet2  31532  fnejoin1  31533  ontgval  31600  unbdqndv1  31669  opnmbllem0  32615  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  sstotbnd2  32743  heiborlem1  32780  heiborlem8  32787  intidl  32998  lsmsat  33313  lssats  33317  lpssat  33318  lssatle  33320  lssat  33321  lsatcvatlem  33354  paddss12  34123  paddasslem17  34140  pmodlem1  34150  pmod1i  34152  pmodl42N  34155  elpcliN  34197  pclfinN  34204  polcon3N  34221  polcon2N  34223  paddunN  34231  pclfinclN  34254  poml5N  34258  osumcllem1N  34260  osumcllem2N  34261  osumcllem3N  34262  pl42lem2N  34284  pl42lem4N  34286  cdlemn5pre  35507  dihord1  35525  dihord2a  35526  dihord2b  35527  dihord5b  35566  dochss  35672  dochdmj1  35697  djhsumss  35714  djhunssN  35716  dochexmidlem2  35768  lclkrslem1  35844  lclkrslem2  35845  lcfrlem2  35850  elrfi  36275  ismrcd1  36279  istopclsd  36281  mrefg2  36288  aomclem2  36643  aomclem6  36647  hbtlem6  36718  hbt  36719  mptrcllem  36939  dfrcl2  36985  relexp0a  37027  trclimalb2  37037  frege81d  37058  k0004ss2  37470  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  uzwo4  38246  ssin0  38248  ixpssmapc  38269  ssinc  38292  ssdec  38293  supxrre3  38482  uzfissfz  38483  ssuzfz  38506  inficc  38608  ressiocsup  38628  ressioosup  38629  ressiooinf  38631  limccog  38687  limclner  38718  cncfmptssg  38755  cncfuni  38772  icccncfext  38773  dvresntr  38806  dvmptresicc  38809  dvbdfbdioolem1  38818  dvdmsscn  38826  dvnxpaek  38832  dvnprodlem2  38837  stoweidlem59  38952  fourierdlem20  39020  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem52  39051  fourierdlem58  39057  fourierdlem64  39063  fourierdlem73  39072  fourierdlem76  39075  fourierdlem80  39079  fourierdlem84  39083  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fourierdlem113  39112  etransclem18  39145  ioorrnopnlem  39200  salincl  39219  intsal  39224  fsumlesge0  39270  sge0cl  39274  sge0supre  39282  sge0less  39285  sge0split  39302  sge0seq  39339  caragensspw  39399  omessre  39400  caragendifcl  39404  caratheodorylem1  39416  0ome  39419  omess0  39424  caragencmpl  39425  hoicvr  39438  hoissrrn  39439  hoicvrrex  39446  ovnlecvr  39448  ovnsslelem  39450  ovnssle  39451  ovnsubaddlem1  39460  hoissrrn2  39468  hoidmv1lelem1  39481  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem4  39488  ovnlecvr2  39500  voncmpl  39511  hspmbl  39519  opnvonmbllem1  39522  ovolval5lem2  39543  ovolval5lem3  39544  vonioolem1  39571  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  issmflem  39613  cnfsmf  39627  incsmflem  39628  smfsssmf  39630  smfadd  39651  decsmflem  39652  smflim  39663  smfres  39675  smfmul  39680  smfpimbor1lem1  39683  smfco  39687  pthdlem1  40972  subsubmgm  41587  elpglem1  42253