Theorem sstri 3943

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 3941	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
4	1, 2, 3	mp2 9	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 209  df-ss 3919

This theorem is referenced by:  snsstp1  4771  snsstp2  4772  uniintsn  4940  elopabran  5528  ssrnres  6158  cossxp  6253  foimacnv  6818  ssimaex  6946  riotassuni  7387  oprabss  7498  dmexg  7876  rnexg  7877  mptmpoopabbrd  8055  fparlem3  8086  fparlem4  8087  snopsuppss  8152  tposssxp  8203  naddunif  8657  naddasslem1  8658  naddasslem2  8659  mapsspw  8853  sbthlem5  9056  sbthlem7  9058  cnvimamptfin  9289  marypha1lem  9372  ordtypelem4  9462  hartogslem1  9483  ttrclco  9666  cottrcl  9667  tc2  9688  frmin  9700  frrlem16  9709  tz9.12lem1  9738  rankval4  9818  rankxpl  9826  rankmapu  9829  rankxplim  9830  djuin  9869  infxpenlem  9962  ackbij1lem18  10185  cflm  10199  fin23lem29  10291  hsmexlem4  10379  hsmexlem5  10380  brdom3  10478  brdom5  10479  brdom4  10480  smobeth  10537  pwfseqlem3  10611  wundm  10679  wunrn  10680  wunex2  10689  ltsopi  10839  dmaddpi  10841  dmmulpi  10842  nqerf  10881  ltrelxr  11236  uzssre  12854  uzwo2  12906  infssuzle  12925  infssuzcl  12926  uzwo3  12937  nn0ssq  12951  nnssq  12952  qsscn  12954  rpnnen1lem3  12973  rpnnen1lem5  12975  dflt2  13143  ioosscn  13405  unitsscn  13497  fzval2  13508  fzossz  13678  fzossnn  13710  injresinj  13790  flval3  13818  uzsup  13866  uzrdgfni  13964  expcl2lem  14079  rpexpcl  14086  expge0  14104  expge1  14105  hashxrcl  14363  seqcoll  14470  xptrrel  14986  trclublem  15001  01sqrexlem3  15261  limsupval2  15497  limsupgre  15498  rlimpm  15517  rlimclim  15563  isercolllem1  15682  isercolllem2  15683  isercoll  15685  caurcvg  15694  caucvg  15696  summolem2a  15732  summolem2  15733  zsum  15735  fsumcvg3  15746  fsumrpcl  15754  fsumge0  15813  climfsum  15838  ackbijnn  15848  prodmolem2a  15954  prodmolem2  15955  zprod  15957  fprodrpcl  15976  fprodge0  16013  fprodge1  16015  rprisefaccl  16043  divalglem8  16424  sadaddlem  16490  lcmfval  16645  isprm3  16707  maxprmfct  16734  pclem  16864  prmreclem1  16942  prmreclem2  16943  prmreclem3  16944  1arith  16953  4sqlem11  16981  ramtlecl  17026  ramcl2lem  17035  ramxrcl  17043  prmgaplem3  17079  prmgaplem4  17080  cshwshashlem1  17121  structfn  17182  strleun  17183  ressbasss  17265  ressbasss2  17267  srngbase  17329  srngplusg  17330  srngmulr  17331  lmodbase  17345  lmodplusg  17346  lmodsca  17347  ipsbase  17356  ipsaddg  17357  ipsmulr  17358  ipssca  17359  ipsvsca  17360  ipsip  17361  phlbase  17366  phlplusg  17367  phlsca  17368  phlvsca  17369  phlip  17370  odrngbas  17423  odrngplusg  17424  odrngmulr  17425  odrngtset  17426  odrngle  17427  odrngds  17428  prdsvallem  17473  prdsval  17474  prdssca  17475  prdsbas  17476  prdsplusg  17477  prdsmulr  17478  prdsvsca  17479  prdsip  17480  prdsle  17481  prdsds  17483  prdstset  17485  prdshom  17486  prdsco  17487  imasbas  17532  imasds  17533  imasplusg  17537  imasmulr  17538  imassca  17539  imasvsca  17540  imasip  17541  imastset  17542  imasle  17543  wunfunc  17924  fullfunc  17931  fthfunc  17932  isfull  17935  isfth  17939  wunnat  17982  dmcoass  18089  catcisolem  18133  catciso  18134  catcoppccl  18140  catcfuccl  18141  catcxpccl  18229  ipobas  18553  ipolerval  18554  ipotset  18555  psdmrn  18595  psss  18602  ledm  18612  lern  18613  dirdm  18622  dirge  18625  mulgfval  19101  mvdco  19475  f1omvdconj  19476  gexex  19883  gsumval3  19937  lssacs  21021  cnfldbas  21415  mpocnfldadd  21416  mpocnfldmul  21418  cnfldcj  21420  cnfldtset  21421  cnfldle  21422  cnfldds  21423  cnfldunif  21424  rge0srg  21477  zntoslem  21595  asplss  21912  aspsubrg  21914  psrass1lem  21972  psrbas  21973  psrplusg  21976  psrmulr  21981  psrsca  21986  psrvscafval  21987  psrass1  22002  psrass23l  22005  psrcom  22006  psrass23  22007  psropprmul  22286  coe1mul2  22319  ofco2  22498  toponsspwpw  22969  dmtopon  22970  leordtval2  23259  lmbrf  23307  lmres  23347  fiuncmp  23451  comppfsc  23579  1stckgenlem  23600  kgencn3  23605  ptbasfi  23628  xkoopn  23636  txcnmpt  23671  txkgen  23699  opnfbas  23889  fmfnfmlem4  24004  tsmsxplem1  24200  trust  24276  restutop  24284  nmoffn  24758  nmofval  24761  nmogelb  24763  nmolb  24764  nmof  24766  qtopbas  24806  tgqioo  24847  re2ndc  24848  iitopon  24928  dfii3  24932  cnheiborlem  25003  bndth  25007  lebnumii  25015  pcoass  25073  cphsqrtcl  25233  lmmbrf  25311  iscauf  25329  caucfil  25332  lmclimf  25353  rrxmval  25454  rrxmet  25457  ovolfioo  25516  ovolficc  25517  ovolficcss  25518  ovolfsf  25520  ovollb  25528  ovolicc2lem3  25568  ovolicc2lem4  25569  ovolicc2  25571  volf  25578  volsup  25605  ovolfs2  25620  uniiccdif  25627  uniioovol  25628  uniiccvol  25629  uniioombllem2  25632  uniioombllem3a  25633  uniioombllem3  25634  uniioombllem4  25635  uniioombllem5  25636  uniioombl  25638  dyadmbllem  25648  dyadmbl  25649  opnmbllem  25650  opnmblALT  25652  volsup2  25654  vitalilem4  25660  vitalilem5  25661  vitali  25662  mbfimaopnlem  25704  mbflimsup  25715  i1f0  25736  i1f1  25739  itg11  25740  itg2mulc  25796  itg2gt0  25809  ellimc2  25926  limcresi  25934  dvreslem  25958  dvres2lem  25959  dvaddbr  25987  dvmulbr  25988  dvlipcn  26043  c1liplem1  26045  lhop1lem  26062  lhop1  26063  lhop2  26064  lhop  26065  dvfsumrlim  26080  ftc1cn  26092  itgsubstlem  26097  itgsubst  26098  itgpowd  26099  mdegleb  26111  mdeglt  26112  mdegldg  26113  mdegxrcl  26114  mdegcl  26116  mdegaddle  26121  mdegmullem  26125  deg1mul3le  26164  ig1peu  26222  ig1pdvds  26227  aacjcl  26378  aannenlem2  26380  aannenlem3  26381  aalioulem2  26384  taylfval  26409  radcnvcl  26467  radcnvlt1  26468  radcnvle  26470  abelth  26491  abelth2  26492  pilem2  26502  pilem3  26503  pige3ALT  26572  recosf1o  26587  resinf1o  26588  tanord1  26589  logcn  26699  dvlog  26703  dvlog2lem  26704  efopn  26710  logtayl  26712  cxpcn3  26800  loglesqrt  26813  ssscongptld  26874  leibpi  26994  efrlim  27021  jensenlem1  27038  jensenlem2  27039  jensen  27040  amgm  27042  lgamgulmlem2  27081  ftalem5  27128  efnnfsumcl  27154  efchtdvds  27210  mpodvdsmulf1o  27245  fsumdvdsmul  27246  dvdsmulf1o  27247  lgsfcl2  27354  2sqlem6  27474  2sqlem8  27477  2sqlem9  27478  rpvmasumlem  27538  rpvmasum2  27563  dchrisum0re  27564  dchrisum0lem3  27570  dchrisum0  27571  rplogsum  27578  dirith2  27579  noextendseq  27718  oldf  27917  leftssno  27953  rightssno  27954  addbdaylem  28097  mulsproplem12  28207  mulsproplem13  28208  mulsproplem14  28209  mulsasslem3  28245  precsexlem11  28297  oncutlt  28344  bdayons  28356  nnssno  28402  axtgcgrrflx  28618  axtgcgrid  28619  axtgsegcon  28620  axtg5seg  28621  axtgbtwnid  28622  axtgpasch  28623  axtgcont1  28624  tgcgr4  28687  motcgrg  28700  tglng  28702  upgrss  29245  pthdivtx  29883  disjxwwlkn  30069  ex-fpar  30620  nmlno0lem  30952  hlimcaui  31395  chsspwh  31406  shsss  31472  chintcli  31490  shsleji  31529  shub1i  31533  shsval2i  31546  lejdii  31697  spanuni  31703  sshhococi  31705  spansnpji  31737  osumcori  31802  5oai  31820  3oalem6  31826  3oai  31827  pjssmii  31840  mayete3i  31887  mayetes3i  31888  nmlnop0iALT  32154  imaelshi  32217  pjnmopi  32307  pjclem1  32354  pjci  32359  mdslmd1lem1  32484  shatomistici  32520  hatomistici  32521  chpssati  32522  xppreima  32807  iundisjfi  32958  iundisj2fi  32959  fprodex01  32987  indsumin  32999  xrsmulgzz  33147  fsumrp0cl  33159  gsummpt2co  33188  cycpmfv2  33254  cycpmrn  33283  rlocbas  33409  rlocaddval  33410  rlocmulval  33411  1fldgenq  33469  xrge0slmod  33494  lsmsnorb  33537  idlsrgbas  33660  idlsrgplusg  33661  idlsrgmulr  33663  idlsrgtset  33664  selvply1rhmlemb  33776  esplyind  33832  vietalem  33836  constrextdg2  34006  ordtconnlem1  34181  xrge0iifhom  34194  lmlimxrge0  34205  lmxrge0  34209  esumcst  34320  esumpfinvallem  34331  esumpfinval  34332  esumpfinvalf  34333  esumcvg  34343  imambfm  34519  elmbfmvol2  34524  sxbrsigalem3  34529  sxbrsigalem2  34543  sxbrsigalem4  34544  sitgclg  34599  eulerpartlem1  34624  eulerpartlemgvv  34633  eulerpartlemgh  34635  eulerpartlemgf  34636  ballotlemfc0  34750  ballotlemfcc  34751  ballotlemiex  34759  ballotlemsup  34762  ballotlemsima  34773  ballotlemrv2  34779  ballotth  34795  signsplypnf  34804  signsply0  34805  rpsqrtcn  34847  itgexpif  34860  fsum2dsub  34861  reprfi2  34877  chtvalz  34883  breprexplemc  34886  breprexpnat  34888  circlemeth  34894  circlemethnat  34895  circlevma  34896  circlemethhgt  34897  hgt750lemd  34902  hgt750lema  34911  tgoldbachgtde  34914  tgoldbachgtda  34915  tgoldbachgt  34917  bnj1145  35248  bnj1286  35274  subfacp1lem2a  35490  erdszelem4  35504  erdszelem5  35505  erdszelem7  35507  erdszelem8  35508  kur14lem7  35522  kur14lem9  35524  resconn  35556  iccllysconn  35560  txpss3v  36186  txprel  36187  limitssson  36219  finminlem  36638  tailf  36695  filnetlem3  36700  onint1  36769  ttcuniun  36830  bj-unrab  37371  bj-2upln1upl  37469  bj-imdirco  37642  bj-rvecssabl  37758  taupilem2  37774  taupi  37775  poimirlem3  38082  poimirlem30  38109  poimirlem31  38110  poimirlem32  38111  broucube  38113  opnmbllem0  38115  mblfinlem1  38116  mblfinlem2  38117  mblfinlem3  38118  mblfinlem4  38119  ismblfin  38120  mbfposadd  38126  cnambfre  38127  itg2addnc  38133  ftc1cnnclem  38150  ftc1cnnc  38151  ftc1anclem3  38154  ftc1anclem7  38158  ftc1anc  38160  ftc2nc  38161  dvreasin  38165  dvreacos  38166  areacirclem1  38167  areacirclem2  38168  areacirc  38172  caures  38219  reheibor  38298  xrnss3v  38840  xrnrel  38841  atlatmstc  39903  atlatle  39904  pmaple  40345  sspadd1  40399  sspadd2  40400  dvrelog2  42641  dvrelog3  42642  rpsscn  42868  sumcubes  42882  redvmptabs  42929  diophin  43313  4rexfrabdioph  43335  6rexfrabdioph  43336  irrapxlem1  43359  irrapx1  43365  rmxyelqirr  43447  monotuz  43478  jm2.27dlem5  43550  hbtlem2  43661  algbase  43711  algaddg  43712  algmulr  43713  algsca  43714  algvsca  43715  arearect  43752  areaquad  43753  rtrclex  44153  trclubgNEW  44154  trclexi  44156  rtrclexi  44157  cnvtrcl0  44162  dfrtrcl5  44165  trrelsuperrel2dg  44207  relexpaddss  44254  brtrclfv2  44263  frege131d  44300  xphe  44317  clsk3nimkb  44576  gneispace  44670  k0004val0  44690  inaex  44833  lhe4.4ex1a  44865  uzmptshftfval  44882  binomcxplemdvbinom  44889  binomcxplemcvg  44890  binomcxplemnotnn0  44892  relopabVD  45436  dmwf  45501  rnwf  45502  fzisoeu  45839  fzsscn  45850  fzssre  45853  fzossuz  45916  zssxr  45932  uzssre2  45941  supminfxr  45998  uzsscn  46009  rpssxr  46014  uzinico  46095  limcresiooub  46176  limcresioolb  46177  limcleqr  46178  limclner  46185  limclr  46189  limsupequzmpt2  46252  liminfval2  46302  liminfequzmpt2  46325  icccncfext  46421  cncficcgt0  46422  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  dvnprodlem2  46481  itgsin0pilem1  46484  itgsinexplem1  46488  itgsinexp  46489  dirkercncflem2  46638  fourierdlem16  46657  fourierdlem18  46659  fourierdlem20  46661  fourierdlem21  46662  fourierdlem22  46663  fourierdlem25  46666  fourierdlem37  46678  fourierdlem42  46683  fourierdlem50  46690  fourierdlem52  46692  fourierdlem62  46702  fourierdlem64  46704  fourierdlem66  46706  fourierdlem68  46708  fourierdlem74  46714  fourierdlem75  46715  fourierdlem76  46716  fourierdlem79  46719  fourierdlem83  46723  fourierdlem95  46735  fourierdlem101  46741  fourierdlem102  46742  fourierdlem103  46743  fourierdlem104  46744  fourierdlem112  46752  fourierdlem114  46754  sqwvfoura  46762  sqwvfourb  46763  fouriersw  46765  etransclem24  46792  etransclem48  46816  sge0sn  46913  sge0tsms  46914  sge0f1o  46916  sge0pr  46928  sge0resplit  46940  sge0split  46943  sge0iunmptlemre  46949  sge0isummpt2  46966  carageniuncllem1  47055  hoicvr  47082  hoicvrrex  47090  hoidmvlelem2  47130  hspmbl  47163  smfmullem4  47328  chnsuslle  47417  lamberte  47442  rehalfge1  47893  prmdvdsfmtnof1lem1  48153  prmdvdsfmtnof  48155  upgrimpthslem2  48490  upgrimpths  48491  oddibas  48755  2zrngbas  48824  2zrng0  48826  dmtposss  49457  tposres3  49462  sepfsepc  49509  uptrlem1  49791  uptrlem2  49792  uptrlem3  49793  uptra  49796  uptrar  49797  uobeqw  49800  uptr2  49802  uptr2a  49803  fucoppcfunc  49993  aacllem  50382  amgmlemALT  50384