Theorem sstri 3931

Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)

Hypotheses

Ref	Expression
sstri.1	⊢ 𝐴 ⊆ 𝐵
sstri.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
sstri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sstri

Step	Hyp	Ref	Expression
1		sstri.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sstri.2	. 2 ⊢ 𝐵 ⊆ 𝐶
3		sstr2 3929	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	1, 2, 3	mp2 9	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  snsstp1  4750  snsstp2  4751  uniintsn  4919  elopabran  5476  ssrnres  6086  cossxp  6179  foimacnv  6742  ssimaex  6862  riotassuni  7282  oprabss  7390  dmexg  7759  rnexg  7760  fabexg  7790  fparlem3  7963  fparlem4  7964  snopsuppss  8004  tposssxp  8055  mapsspw  8675  sbthlem5  8883  sbthlem7  8885  cnvimamptfin  9129  marypha1lem  9201  ordtypelem4  9289  hartogslem1  9310  ttrclco  9485  cottrcl  9486  tc2  9509  frmin  9516  frrlem16  9525  tz9.12lem1  9554  rankval4  9634  rankxpl  9642  rankmapu  9645  rankxplim  9646  djuin  9685  infxpenlem  9778  ackbij1lem18  10002  cflm  10015  fin23lem29  10106  hsmexlem4  10194  hsmexlem5  10195  brdom3  10293  brdom5  10294  brdom4  10295  smobeth  10351  pwfseqlem3  10425  wundm  10493  wunrn  10494  wunex2  10503  ltsopi  10653  dmaddpi  10655  dmmulpi  10656  nqerf  10695  ltrelxr  11045  uzssre  12613  uzwo2  12661  infssuzle  12680  infssuzcl  12681  uzwo3  12692  nn0ssq  12706  nnssq  12707  qsscn  12709  rpnnen1lem3  12728  rpnnen1lem5  12730  dflt2  12891  ioosscn  13150  unitsscn  13241  fzval2  13251  fzossz  13416  fzossnn  13445  injresinj  13517  flval3  13544  uzsup  13592  uzrdgfni  13687  expcl2lem  13803  rpexpcl  13810  expge0  13828  expge1  13829  hashxrcl  14081  seqcoll  14187  xptrrel  14700  trclublem  14715  sqrlem3  14965  limsupval2  15198  limsupgre  15199  rlimpm  15218  rlimclim  15264  isercolllem1  15385  isercolllem2  15386  isercoll  15388  caurcvg  15397  caucvg  15399  summolem2a  15436  summolem2  15437  zsum  15439  fsumcvg3  15450  fsumrpcl  15458  fsumge0  15516  climfsum  15541  ackbijnn  15549  prodmolem2a  15653  prodmolem2  15654  zprod  15656  fprodrpcl  15675  fprodge0  15712  fprodge1  15714  rprisefaccl  15742  divalglem8  16118  sadaddlem  16182  lcmfval  16335  isprm3  16397  maxprmfct  16423  pclem  16548  prmreclem1  16626  prmreclem2  16627  prmreclem3  16628  1arith  16637  4sqlem11  16665  ramtlecl  16710  ramcl2lem  16719  ramxrcl  16727  prmgaplem3  16763  prmgaplem4  16764  cshwshashlem1  16806  structfn  16866  strleun  16867  srngbase  17029  srngplusg  17030  srngmulr  17031  lmodbase  17045  lmodplusg  17046  lmodsca  17047  ipsbase  17056  ipsaddg  17057  ipsmulr  17058  ipssca  17059  ipsvsca  17060  ipsip  17061  phlbase  17066  phlplusg  17067  phlsca  17068  phlvsca  17069  phlip  17070  odrngbas  17123  odrngplusg  17124  odrngmulr  17125  odrngtset  17126  odrngle  17127  odrngds  17128  prdsvallem  17174  prdsval  17175  prdssca  17176  prdsbas  17177  prdsplusg  17178  prdsmulr  17179  prdsvsca  17180  prdsip  17181  prdsle  17182  prdsds  17184  prdstset  17186  prdshom  17187  prdsco  17188  imasbas  17232  imasds  17233  imasplusg  17237  imasmulr  17238  imassca  17239  imasvsca  17240  imasip  17241  imastset  17242  imasle  17243  wunfunc  17623  wunfuncOLD  17624  fullfunc  17631  fthfunc  17632  isfull  17635  isfth  17639  wunnat  17681  wunnatOLD  17682  dmcoass  17790  catcisolem  17834  catciso  17835  catcoppccl  17841  catcoppcclOLD  17842  catcfuccl  17843  catcfucclOLD  17844  catcxpccl  17933  catcxpcclOLD  17934  ipobas  18258  ipolerval  18259  ipotset  18260  psdmrn  18300  psss  18307  ledm  18317  lern  18318  dirdm  18327  dirge  18330  mulgfval  18711  mvdco  19062  f1omvdconj  19063  gexex  19463  gsumval3  19517  lssacs  20238  cnfldbas  20610  cnfldadd  20611  cnfldmul  20612  cnfldcj  20613  cnfldtset  20614  cnfldle  20615  cnfldds  20616  cnfldunif  20617  rge0srg  20678  zntoslem  20773  asplss  21087  aspsubrg  21089  psrass1lemOLD  21152  psrass1lem  21155  psrbas  21156  psrplusg  21159  psrmulr  21162  psrsca  21167  psrvscafval  21168  psrass1  21183  psrass23l  21186  psrcom  21187  psrass23  21188  psropprmul  21418  coe1mul2  21449  ofco2  21609  toponsspwpw  22080  dmtopon  22081  leordtval2  22372  lmbrf  22420  lmres  22460  fiuncmp  22564  comppfsc  22692  1stckgenlem  22713  kgencn3  22718  ptbasfi  22741  xkoopn  22749  txcnmpt  22784  txkgen  22812  opnfbas  23002  fmfnfmlem4  23117  tsmsxplem1  23313  trust  23390  restutop  23398  nmoffn  23884  nmofval  23887  nmogelb  23889  nmolb  23890  nmof  23892  qtopbas  23932  tgqioo  23972  re2ndc  23973  iitopon  24051  dfii3  24055  iimulcn  24110  cnheiborlem  24126  bndth  24130  lebnumii  24138  reparphti  24169  pcoass  24196  cphsqrtcl  24357  lmmbrf  24435  iscauf  24453  caucfil  24456  lmclimf  24477  rrxmval  24578  rrxmet  24581  ovolfioo  24640  ovolficc  24641  ovolficcss  24642  ovolfsf  24644  ovollb  24652  ovolicc2lem3  24692  ovolicc2lem4  24693  ovolicc2  24695  volf  24702  volsup  24729  ovolfs2  24744  uniiccdif  24751  uniioovol  24752  uniiccvol  24753  uniioombllem2  24756  uniioombllem3a  24757  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  uniioombl  24762  dyadmbllem  24772  dyadmbl  24773  opnmbllem  24774  opnmblALT  24776  volsup2  24778  vitalilem4  24784  vitalilem5  24785  vitali  24786  mbfimaopnlem  24828  mbflimsup  24839  i1f0  24860  i1f1  24863  itg11  24864  itg2mulc  24921  itg2gt0  24934  ellimc2  25050  limcresi  25058  dvreslem  25082  dvres2lem  25083  dvaddbr  25111  dvmulbr  25112  dvlipcn  25167  c1liplem1  25169  lhop1lem  25186  lhop1  25187  lhop2  25188  lhop  25189  dvfsumrlim  25204  ftc1cn  25216  itgsubstlem  25221  itgsubst  25222  itgpowd  25223  mdegleb  25238  mdeglt  25239  mdegldg  25240  mdegxrcl  25241  mdegcl  25243  mdegaddle  25248  mdegmullem  25252  deg1mul3le  25290  ig1peu  25345  ig1pdvds  25350  aacjcl  25496  aannenlem2  25498  aannenlem3  25499  aalioulem2  25502  taylfval  25527  radcnvcl  25585  radcnvlt1  25586  radcnvle  25588  abelth  25609  abelth2  25610  pilem2  25620  pilem3  25621  pige3ALT  25685  recosf1o  25700  resinf1o  25701  tanord1  25702  logcn  25811  dvlog  25815  dvlog2lem  25816  efopn  25822  logtayl  25824  cxpcn3  25910  loglesqrt  25920  ssscongptld  25981  leibpi  26101  efrlim  26128  jensenlem1  26145  jensenlem2  26146  jensen  26147  amgm  26149  lgamgulmlem2  26188  ftalem5  26235  efnnfsumcl  26261  efchtdvds  26317  dvdsmulf1o  26352  fsumdvdsmul  26353  lgsfcl2  26460  2sqlem6  26580  2sqlem8  26583  2sqlem9  26584  rpvmasumlem  26644  rpvmasum2  26669  dchrisum0re  26670  dchrisum0lem3  26676  dchrisum0  26677  rplogsum  26684  dirith2  26685  axtgcgrrflx  26832  axtgcgrid  26833  axtgsegcon  26834  axtg5seg  26835  axtgbtwnid  26836  axtgpasch  26837  axtgcont1  26838  tgcgr4  26901  motcgrg  26914  tglng  26916  upgrss  27467  pthdivtx  28106  disjxwwlkn  28287  ex-fpar  28835  nmlno0lem  29164  hlimcaui  29607  chsspwh  29618  shsss  29684  chintcli  29702  shsleji  29741  shub1i  29745  shsval2i  29758  lejdii  29909  spanuni  29915  sshhococi  29917  spansnpji  29949  osumcori  30014  5oai  30032  3oalem6  30038  3oai  30039  pjssmii  30052  mayete3i  30099  mayetes3i  30100  nmlnop0iALT  30366  imaelshi  30429  pjnmopi  30519  pjclem1  30566  pjci  30571  mdslmd1lem1  30696  shatomistici  30732  hatomistici  30733  chpssati  30734  xppreima  30992  iundisjfi  31126  iundisj2fi  31127  fprodex01  31148  xrsmulgzz  31296  fsumrp0cl  31313  gsummpt2co  31317  cycpmfv2  31390  cycpmrn  31419  xrge0slmod  31557  lsmsnorb  31588  idlsrgbas  31658  idlsrgplusg  31659  idlsrgmulr  31661  idlsrgtset  31662  ordtconnlem1  31883  xrge0iifhom  31896  lmlimxrge0  31907  lmxrge0  31911  indsumin  31999  esumcst  32040  esumpfinvallem  32051  esumpfinval  32052  esumpfinvalf  32053  esumcvg  32063  imambfm  32238  elmbfmvol2  32243  sxbrsigalem3  32248  sxbrsigalem2  32262  sxbrsigalem4  32263  sitgclg  32318  eulerpartlem1  32343  eulerpartlemgvv  32352  eulerpartlemgh  32354  eulerpartlemgf  32355  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemiex  32477  ballotlemsup  32480  ballotlemsima  32491  ballotlemrv2  32497  ballotth  32513  signsplypnf  32538  signsply0  32539  rpsqrtcn  32582  itgexpif  32595  fsum2dsub  32596  reprfi2  32612  chtvalz  32618  breprexplemc  32621  breprexpnat  32623  circlemeth  32629  circlemethnat  32630  circlevma  32631  circlemethhgt  32632  hgt750lemd  32637  hgt750lema  32646  tgoldbachgtde  32649  tgoldbachgtda  32650  tgoldbachgt  32652  bnj1145  32982  bnj1286  33008  subfacp1lem2a  33151  erdszelem4  33165  erdszelem5  33166  erdszelem7  33168  erdszelem8  33169  kur14lem7  33183  kur14lem9  33185  cvxpconn  33213  cvxsconn  33214  resconn  33217  iccllysconn  33221  noextendseq  33879  oldf  34050  leftssno  34072  rightssno  34073  txpss3v  34189  txprel  34190  limitssson  34222  finminlem  34516  tailf  34573  filnetlem3  34578  onint1  34647  bj-unrab  35123  bj-2upln1upl  35223  bj-imdirco  35370  bj-rvecssabl  35486  taupilem2  35502  taupi  35503  poimirlem3  35789  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  broucube  35820  opnmbllem0  35822  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  mbfposadd  35833  cnambfre  35834  itg2addnc  35840  ftc1cnnclem  35857  ftc1cnnc  35858  ftc1anclem3  35861  ftc1anclem7  35865  ftc1anc  35867  ftc2nc  35868  dvreasin  35872  dvreacos  35873  areacirclem1  35874  areacirclem2  35875  areacirc  35879  caures  35927  reheibor  36006  xrnss3v  36509  xrnrel  36510  atlatmstc  37340  atlatle  37341  pmaple  37782  sspadd1  37836  sspadd2  37837  dvrelog2  40079  dvrelog3  40080  diophin  40601  4rexfrabdioph  40627  6rexfrabdioph  40628  irrapxlem1  40651  irrapx1  40657  monotuz  40770  jm2.27dlem5  40842  hbtlem2  40956  algbase  41010  algaddg  41011  algmulr  41012  algsca  41013  algvsca  41014  arearect  41053  areaquad  41054  rtrclex  41232  trclubgNEW  41233  trclexi  41235  rtrclexi  41236  cnvtrcl0  41241  dfrtrcl5  41244  trrelsuperrel2dg  41286  relexpaddss  41333  brtrclfv2  41342  frege131d  41379  xphe  41396  clsk3nimkb  41657  gneispace  41751  k0004val0  41771  inaex  41922  lhe4.4ex1a  41954  uzmptshftfval  41971  binomcxplemdvbinom  41978  binomcxplemcvg  41979  binomcxplemnotnn0  41981  relopabVD  42528  fzisoeu  42846  fzsscn  42857  fzssre  42860  fzossuz  42927  zssxr  42944  uzssre2  42954  supminfxr  43011  uzsscn  43023  rpssxr  43028  uzinico  43105  limcresiooub  43190  limcresioolb  43191  limcleqr  43192  limclner  43199  limclr  43203  limsupequzmpt2  43266  liminfval2  43316  liminfequzmpt2  43339  icccncfext  43435  cncficcgt0  43436  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem1  43494  dvnprodlem2  43495  itgsin0pilem1  43498  itgsinexplem1  43502  itgsinexp  43503  dirkercncflem2  43652  fourierdlem16  43671  fourierdlem18  43673  fourierdlem20  43675  fourierdlem21  43676  fourierdlem22  43677  fourierdlem25  43680  fourierdlem37  43692  fourierdlem42  43697  fourierdlem50  43704  fourierdlem52  43706  fourierdlem62  43716  fourierdlem64  43718  fourierdlem66  43720  fourierdlem68  43722  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem79  43733  fourierdlem83  43737  fourierdlem95  43749  fourierdlem101  43755  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem112  43766  fourierdlem114  43768  sqwvfoura  43776  sqwvfourb  43777  fouriersw  43779  etransclem24  43806  etransclem48  43830  sge0sn  43924  sge0tsms  43925  sge0f1o  43927  sge0pr  43939  sge0resplit  43951  sge0split  43954  sge0iunmptlemre  43960  sge0isummpt2  43977  carageniuncllem1  44066  hoicvr  44093  hoicvrrex  44101  hoidmvlelem2  44141  hspmbl  44174  smfmullem4  44339  prmdvdsfmtnof1lem1  45047  prmdvdsfmtnof  45049  oddibas  45378  2zrngbas  45505  2zrng0  45507  sepfsepc  46232  aacllem  46516  amgmlemALT  46518