Theorem sstri 3976

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

Syntax hints:   ⊆ 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:  snsstp1  4749  snsstp2  4750  uniintsn  4913  ssrnres  6035  cossxp  6123  foimacnv  6632  ssimaex  6748  riotassuni  7154  oprabss  7260  dmexg  7613  rnexg  7614  fabexg  7639  fparlem3  7809  fparlem4  7810  snopsuppss  7845  tposssxp  7896  mapsspw  8442  sbthlem5  8631  sbthlem7  8633  cnvimamptfin  8825  marypha1lem  8897  ordtypelem4  8985  hartogslem1  9006  tc2  9184  tz9.12lem1  9216  rankval4  9296  rankxpl  9304  rankmapu  9307  rankxplim  9308  djuin  9347  infxpenlem  9439  ackbij1lem18  9659  cflm  9672  fin23lem29  9763  hsmexlem4  9851  hsmexlem5  9852  brdom3  9950  brdom5  9951  brdom4  9952  smobeth  10008  pwfseqlem3  10082  wundm  10150  wunrn  10151  wunex2  10160  ltsopi  10310  dmaddpi  10312  dmmulpi  10313  nqerf  10352  ltrelxr  10702  uzwo2  12313  infssuzle  12332  infssuzcl  12333  uzwo3  12344  nn0ssq  12357  nnssq  12358  qsscn  12360  rpnnen1lem3  12379  rpnnen1lem5  12381  dflt2  12542  fzval2  12896  fzossz  13058  fzossnn  13087  injresinj  13159  flval3  13186  uzsup  13232  uzrdgfni  13327  expcl2lem  13442  rpexpcl  13449  expge0  13466  expge1  13467  hashxrcl  13719  seqcoll  13823  wrdexgOLD  13873  xptrrel  14340  trclublem  14355  sqrlem3  14604  limsupval2  14837  limsupgre  14838  rlimpm  14857  rlimclim  14903  isercolllem1  15021  isercolllem2  15022  isercoll  15024  caurcvg  15033  caucvg  15035  summolem2a  15072  summolem2  15073  zsum  15075  fsumcvg3  15086  fsumrpcl  15094  fsumge0  15150  climfsum  15175  ackbijnn  15183  prodmolem2a  15288  prodmolem2  15289  zprod  15291  fprodrpcl  15310  fprodge0  15347  fprodge1  15349  rprisefaccl  15377  divalglem8  15751  sadaddlem  15815  lcmfval  15965  isprm3  16027  maxprmfct  16053  pclem  16175  prmreclem1  16252  prmreclem2  16253  prmreclem3  16254  1arith  16263  4sqlem11  16291  ramtlecl  16336  ramcl2lem  16345  ramxrcl  16353  prmgaplem3  16389  prmgaplem4  16390  cshwshashlem1  16429  structfn  16500  strleun  16591  srngbase  16628  srngplusg  16629  srngmulr  16630  lmodbase  16637  lmodplusg  16638  lmodsca  16639  ipsbase  16644  ipsaddg  16645  ipsmulr  16646  ipssca  16647  ipsvsca  16648  ipsip  16649  phlbase  16654  phlplusg  16655  phlsca  16656  phlvsca  16657  phlip  16658  odrngbas  16680  odrngplusg  16681  odrngmulr  16682  odrngtset  16683  odrngle  16684  odrngds  16685  prdsval  16728  prdssca  16729  prdsbas  16730  prdsplusg  16731  prdsmulr  16732  prdsvsca  16733  prdsip  16734  prdsle  16735  prdsds  16737  prdstset  16739  prdshom  16740  prdsco  16741  imasbas  16785  imasds  16786  imasplusg  16790  imasmulr  16791  imassca  16792  imasvsca  16793  imasip  16794  imastset  16795  imasle  16796  wunfunc  17169  fullfunc  17176  fthfunc  17177  isfull  17180  isfth  17184  wunnat  17226  dmcoass  17326  catcisolem  17366  catciso  17367  catcoppccl  17368  catcfuccl  17369  catcxpccl  17457  ipobas  17765  ipolerval  17766  ipotset  17767  psdmrn  17817  psss  17824  ledm  17834  lern  17835  dirdm  17844  dirge  17847  mulgfval  18226  mvdco  18573  f1omvdconj  18574  gexex  18973  gsumval3  19027  lssacs  19739  asplss  20103  aspsubrg  20105  psrass1lem  20157  psrbas  20158  psrplusg  20161  psrmulr  20164  psrsca  20169  psrvscafval  20170  psrass1  20185  psrass23l  20188  psrcom  20189  psrass23  20190  psropprmul  20406  coe1mul2  20437  cnfldbas  20549  cnfldadd  20550  cnfldmul  20551  cnfldcj  20552  cnfldtset  20553  cnfldle  20554  cnfldds  20555  cnfldunif  20556  rge0srg  20616  zntoslem  20703  ofco2  21060  toponsspwpw  21530  dmtopon  21531  leordtval2  21820  lmbrf  21868  lmres  21908  fiuncmp  22012  comppfsc  22140  1stckgenlem  22161  kgencn3  22166  ptbasfi  22189  xkoopn  22197  txcnmpt  22232  txkgen  22260  opnfbas  22450  fmfnfmlem4  22565  tsmsxplem1  22761  trust  22838  restutop  22846  nmoffn  23320  nmofval  23323  nmogelb  23325  nmolb  23326  nmof  23328  qtopbas  23368  tgqioo  23408  re2ndc  23409  iitopon  23487  dfii3  23491  iimulcn  23542  cnheiborlem  23558  bndth  23562  lebnumii  23570  reparphti  23601  pcoass  23628  cphsqrtcl  23788  lmmbrf  23865  iscauf  23883  caucfil  23886  lmclimf  23907  rrxmval  24008  rrxmet  24011  ovolfioo  24068  ovolficc  24069  ovolficcss  24070  ovolfsf  24072  ovollb  24080  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2  24123  volf  24130  volsup  24157  ovolfs2  24172  uniiccdif  24179  uniioovol  24180  uniiccvol  24181  uniioombllem2  24184  uniioombllem3a  24185  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  uniioombl  24190  dyadmbllem  24200  dyadmbl  24201  opnmbllem  24202  opnmblALT  24204  volsup2  24206  vitalilem4  24212  vitalilem5  24213  vitali  24214  mbfimaopnlem  24256  mbflimsup  24267  i1f0  24288  i1f1  24291  itg11  24292  itg2mulc  24348  itg2gt0  24361  ellimc2  24475  limcresi  24483  dvreslem  24507  dvres2lem  24508  dvaddbr  24535  dvmulbr  24536  dvlipcn  24591  c1liplem1  24593  lhop1lem  24610  lhop1  24611  lhop2  24612  lhop  24613  dvfsumrlim  24628  ftc1cn  24640  itgsubstlem  24645  itgsubst  24646  mdegleb  24658  mdeglt  24659  mdegldg  24660  mdegxrcl  24661  mdegcl  24663  mdegaddle  24668  mdegmullem  24672  deg1mul3le  24710  ig1peu  24765  ig1pdvds  24770  aacjcl  24916  aannenlem2  24918  aannenlem3  24919  aalioulem2  24922  taylfval  24947  radcnvcl  25005  radcnvlt1  25006  radcnvle  25008  abelth  25029  abelth2  25030  pilem2  25040  pilem3  25041  pige3ALT  25105  recosf1o  25119  resinf1o  25120  tanord1  25121  logcn  25230  dvlog  25234  dvlog2lem  25235  efopn  25241  logtayl  25243  cxpcn3  25329  loglesqrt  25339  ssscongptld  25400  leibpi  25520  efrlim  25547  jensenlem1  25564  jensenlem2  25565  jensen  25566  amgm  25568  lgamgulmlem2  25607  ftalem5  25654  efnnfsumcl  25680  efchtdvds  25736  dvdsmulf1o  25771  fsumdvdsmul  25772  lgsfcl2  25879  2sqlem6  25999  2sqlem8  26002  2sqlem9  26003  rpvmasumlem  26063  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem3  26095  dchrisum0  26096  rplogsum  26103  dirith2  26104  axtgcgrrflx  26248  axtgcgrid  26249  axtgsegcon  26250  axtg5seg  26251  axtgbtwnid  26252  axtgpasch  26253  axtgcont1  26254  tgcgr4  26317  motcgrg  26330  tglng  26332  upgrss  26873  pthdivtx  27510  disjxwwlkn  27692  ex-fpar  28241  nmlno0lem  28570  hlimcaui  29013  chsspwh  29024  shsss  29090  chintcli  29108  shsleji  29147  shub1i  29151  shsval2i  29164  lejdii  29315  spanuni  29321  sshhococi  29323  spansnpji  29355  osumcori  29420  5oai  29438  3oalem6  29444  3oai  29445  pjssmii  29458  mayete3i  29505  mayetes3i  29506  nmlnop0iALT  29772  imaelshi  29835  pjnmopi  29925  pjclem1  29972  pjci  29977  mdslmd1lem1  30102  shatomistici  30138  hatomistici  30139  chpssati  30140  xppreima  30394  iundisjfi  30519  iundisj2fi  30520  fprodex01  30541  xrsmulgzz  30665  fsumrp0cl  30682  gsummpt2co  30686  cycpmfv2  30756  cycpmrn  30785  xrge0slmod  30917  lsmsnorb  30945  unitsscn  31139  ordtconnlem1  31167  xrge0iifhom  31180  lmlimxrge0  31191  lmxrge0  31195  indsumin  31281  esumcst  31322  esumpfinvallem  31333  esumpfinval  31334  esumpfinvalf  31335  esumcvg  31345  imambfm  31520  elmbfmvol2  31525  sxbrsigalem3  31530  sxbrsigalem2  31544  sxbrsigalem4  31545  sitgclg  31600  eulerpartlem1  31625  eulerpartlemgvv  31634  eulerpartlemgh  31636  eulerpartlemgf  31637  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemiex  31759  ballotlemsup  31762  ballotlemsdom  31769  ballotlemsima  31773  ballotlemrv2  31779  ballotth  31795  signsplypnf  31820  signsply0  31821  rpsqrtcn  31864  itgexpif  31877  fsum2dsub  31878  reprfi2  31894  chtvalz  31900  breprexplemc  31903  breprexpnat  31905  circlemeth  31911  circlemethnat  31912  circlevma  31913  circlemethhgt  31914  hgt750lemd  31919  hgt750lema  31928  tgoldbachgtde  31931  tgoldbachgtda  31932  tgoldbachgt  31934  bnj1145  32265  bnj1286  32291  subfacp1lem2a  32427  erdszelem4  32441  erdszelem5  32442  erdszelem7  32444  erdszelem8  32445  kur14lem7  32459  kur14lem9  32461  cvxpconn  32489  cvxsconn  32490  resconn  32493  iccllysconn  32497  noextendseq  33174  txpss3v  33339  txprel  33340  limitssson  33372  finminlem  33666  tailf  33723  filnetlem3  33728  onint1  33797  bj-unrab  34247  bj-2upln1upl  34339  bj-rvecssabl  34590  taupilem2  34606  taupi  34607  poimirlem3  34910  poimirlem30  34937  poimirlem31  34938  poimirlem32  34939  broucube  34941  opnmbllem0  34943  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  mbfposadd  34954  cnambfre  34955  itg2addnc  34961  ftc1cnnclem  34980  ftc1cnnc  34981  ftc1anclem3  34984  ftc1anclem7  34988  ftc1anc  34990  ftc2nc  34991  dvreasin  34995  dvreacos  34996  areacirclem1  34997  areacirclem2  34998  areacirc  35002  caures  35050  reheibor  35132  xrnss3v  35639  xrnrel  35640  atlatmstc  36470  atlatle  36471  pmaple  36912  sspadd1  36966  sspadd2  36967  diophin  39418  4rexfrabdioph  39444  6rexfrabdioph  39445  irrapxlem1  39468  irrapx1  39474  monotuz  39587  jm2.27dlem5  39659  hbtlem2  39773  algbase  39827  algaddg  39828  algmulr  39829  algsca  39830  algvsca  39831  itgpowd  39870  arearect  39871  areaquad  39872  rtrclex  40026  trclubgNEW  40027  trclexi  40029  rtrclexi  40030  cnvtrcl0  40035  dfrtrcl5  40038  trrelsuperrel2dg  40065  relexpaddss  40112  brtrclfv2  40121  frege131d  40158  xphe  40176  clsk3nimkb  40439  gneispace  40533  k0004val0  40553  inaex  40682  lhe4.4ex1a  40710  uzmptshftfval  40727  binomcxplemdvbinom  40734  binomcxplemcvg  40735  binomcxplemnotnn0  40737  relopabVD  41284  fzisoeu  41616  fzsscn  41627  fzssre  41630  fzossuz  41699  uzssre  41718  zssxr  41719  uzssre2  41729  supminfxr  41789  uzsscn  41801  rpssxr  41806  ioosscn  41818  uzinico  41885  limcresiooub  41972  limcresioolb  41973  limcleqr  41974  limclner  41981  limclr  41985  limsupequzmpt2  42048  liminfval2  42098  liminfequzmpt2  42121  icccncfext  42219  cncficcgt0  42220  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnprodlem1  42280  dvnprodlem2  42281  itgsin0pilem1  42284  itgsinexplem1  42288  itgsinexp  42289  dirkercncflem2  42438  fourierdlem16  42457  fourierdlem18  42459  fourierdlem20  42461  fourierdlem21  42462  fourierdlem22  42463  fourierdlem25  42466  fourierdlem37  42478  fourierdlem42  42483  fourierdlem50  42490  fourierdlem52  42492  fourierdlem62  42502  fourierdlem64  42504  fourierdlem66  42506  fourierdlem68  42508  fourierdlem74  42514  fourierdlem75  42515  fourierdlem76  42516  fourierdlem79  42519  fourierdlem83  42523  fourierdlem95  42535  fourierdlem101  42541  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  fourierdlem114  42554  sqwvfoura  42562  sqwvfourb  42563  fouriersw  42565  etransclem24  42592  etransclem48  42616  sge0sn  42710  sge0tsms  42711  sge0f1o  42713  sge0pr  42725  sge0resplit  42737  sge0split  42740  sge0iunmptlemre  42746  sge0isummpt2  42763  carageniuncllem1  42852  hoicvr  42879  hoicvrrex  42887  hoidmvlelem2  42927  hspmbl  42960  smfmullem4  43118  prmdvdsfmtnof1lem1  43795  prmdvdsfmtnof  43797  oddibas  44129  2zrngbas  44256  2zrng0  44258  aacllem  44951  amgmlemALT  44953