Theorem sstri 3612

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

Hypotheses

Ref	Expression
sstri.1	|- A C_ B
sstri.2	|- B C_ C

Assertion

Ref	Expression
sstri	|- A C_ C

Proof of Theorem sstri

Step	Hyp	Ref	Expression
1		sstri.1	. 2 |- A C_ B
2		sstri.2	. 2 |- B C_ C
3		sstr2 3610	. 2 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
4	1, 2, 3	mp2 9	1 |- A C_ C

Syntax hints:   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  snsstp1  4347  snsstp2  4348  uniintsn  4514  ssrnres  5572  cossxp  5658  foimacnv  6154  ssimaex  6263  riotassuni  6648  oprabss  6746  dmexg  7097  rnexg  7098  fabexg  7122  fparlem3  7279  fparlem4  7280  snopsuppss  7310  tposssxp  7356  mapsspw  7893  sbthlem5  8074  sbthlem7  8076  cnvimamptfin  8267  marypha1lem  8339  ordtypelem4  8426  hartogslem1  8447  tc2  8618  tz9.12lem1  8650  rankval4  8730  rankxpl  8738  rankmapu  8741  rankxplim  8742  infxpenlem  8836  ackbij1lem18  9059  cflm  9072  fin23lem29  9163  hsmexlem4  9251  hsmexlem5  9252  brdom3  9350  brdom5  9351  brdom4  9352  smobeth  9408  pwfseqlem3  9482  wundm  9550  wunrn  9551  wunex2  9560  ltsopi  9710  dmaddpi  9712  dmmulpi  9713  nqerf  9752  ltrelxr  10099  nnsscn  11025  nn0sscn  11297  uzwo2  11752  infssuzle  11771  infssuzcl  11772  uzwo3  11783  nn0ssq  11796  nnssq  11797  qsscn  11799  rpnnen1lem3  11816  rpnnen1lem5  11818  rpnnen1lem3OLD  11822  rpnnen1lem5OLD  11824  dflt2  11981  fzval2  12329  fzof  12467  fzossnn  12516  fzo0ssnn0OLD  12549  injresinj  12589  flval3  12616  uzsup  12662  uzrdgfni  12757  expcl2lem  12872  rpexpcl  12879  expge0  12896  expge1  12897  hashxrcl  13148  seqcoll  13248  wrdexg  13315  xptrrel  13719  trclublem  13734  sqrlem3  13985  limsupval2  14211  limsupgre  14212  rlimpm  14231  rlimclim  14277  isercolllem1  14395  isercolllem2  14396  isercoll  14398  caurcvg  14407  caucvg  14409  summolem2a  14446  summolem2  14447  zsum  14449  fsumcvg3  14460  fsumrpcl  14468  fsumge0  14527  climfsum  14552  ackbijnn  14560  prodmolem2a  14664  prodmolem2  14665  zprod  14667  fprodrpcl  14686  fprodge0  14724  fprodge1  14726  rprisefaccl  14754  divalglem8  15123  sadaddlem  15188  lcmfval  15334  isprm3  15396  maxprmfct  15421  pclem  15543  prmreclem1  15620  prmreclem2  15621  prmreclem3  15622  1arith  15631  4sqlem11  15659  ramtlecl  15704  ramcl2lem  15713  ramxrcl  15721  prmgaplem3  15757  prmgaplem4  15758  cshwshashlem1  15802  structfn  15874  strlemor1OLD  15969  strleun  15972  srngbase  16009  srngplusg  16010  srngmulr  16011  lmodbase  16018  lmodplusg  16019  lmodsca  16020  ipsbase  16025  ipsaddg  16026  ipsmulr  16027  ipssca  16028  ipsvsca  16029  ipsip  16030  phlbase  16035  phlplusg  16036  phlsca  16037  phlvsca  16038  phlip  16039  odrngbas  16067  odrngplusg  16068  odrngmulr  16069  odrngtset  16070  odrngle  16071  odrngds  16072  prdsval  16115  prdssca  16116  prdsbas  16117  prdsplusg  16118  prdsmulr  16119  prdsvsca  16120  prdsip  16121  prdsle  16122  prdsds  16124  prdstset  16126  prdshom  16127  prdsco  16128  imasbas  16172  imasds  16173  imasplusg  16177  imasmulr  16178  imassca  16179  imasvsca  16180  imasip  16181  imastset  16182  imasle  16183  wunfunc  16559  fullfunc  16566  fthfunc  16567  isfull  16570  isfth  16574  wunnat  16616  dmcoass  16716  catcisolem  16756  catciso  16757  catcoppccl  16758  catcfuccl  16759  catcxpccl  16847  ipobas  17155  ipolerval  17156  ipotset  17157  psdmrn  17207  psss  17214  ledm  17224  lern  17225  dirdm  17234  dirge  17237  mvdco  17865  f1omvdconj  17866  gexex  18256  gsumval3  18308  lssacs  18967  asplss  19329  aspsubrg  19331  psrass1lem  19377  psrbas  19378  psrplusg  19381  psrmulr  19384  psrsca  19389  psrvscafval  19390  psrass1  19405  psrass23l  19408  psrcom  19409  psrass23  19410  psropprmul  19608  coe1mul2  19639  cnfldbas  19750  cnfldadd  19751  cnfldmul  19752  cnfldcj  19753  cnfldtset  19754  cnfldle  19755  cnfldds  19756  cnfldunif  19757  rge0srg  19817  zntoslem  19905  ofco2  20257  toponsspwpw  20726  dmtopon  20727  leordtval2  21016  lmbrf  21064  lmres  21104  fiuncmp  21207  comppfsc  21335  1stckgenlem  21356  kgencn3  21361  ptbasfi  21384  xkoopn  21392  txcnmpt  21427  txkgen  21455  opnfbas  21646  fmfnfmlem4  21761  tsmsxplem1  21956  trust  22033  restutop  22041  nmoffn  22515  nmofval  22518  nmogelb  22520  nmolb  22521  nmof  22523  qtopbas  22563  tgqioo  22603  re2ndc  22604  iitopon  22682  dfii3  22686  iimulcn  22737  cnheiborlem  22753  bndth  22757  lebnumii  22765  reparphti  22797  pcoass  22824  cphsqrtcl  22984  lmmbrf  23060  iscauf  23078  caucfil  23081  lmclimf  23102  rrxmval  23188  rrxmet  23191  ovolfioo  23236  ovolficc  23237  ovolficcss  23238  ovolfsf  23240  ovollb  23247  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2  23290  volf  23297  volsup  23324  ovolfs2  23339  uniiccdif  23346  uniioovol  23347  uniiccvol  23348  uniioombllem2  23351  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombl  23357  dyadmbllem  23367  dyadmbl  23368  opnmbllem  23369  opnmblALT  23371  volsup2  23373  vitalilem4  23380  vitalilem5  23381  vitali  23382  mbfimaopnlem  23422  mbflimsup  23433  i1f0  23454  i1f1  23457  itg11  23458  itg2mulc  23514  itg2gt0  23527  ellimc2  23641  limcresi  23649  dvreslem  23673  dvres2lem  23674  dvaddbr  23701  dvmulbr  23702  dvlipcn  23757  c1liplem1  23759  lhop1lem  23776  lhop1  23777  lhop2  23778  lhop  23779  dvfsumrlim  23794  ftc1cn  23806  itgsubstlem  23811  itgsubst  23812  mdegleb  23824  mdeglt  23825  mdegldg  23826  mdegxrcl  23827  mdegcl  23829  mdegaddle  23834  mdegmullem  23838  deg1mul3le  23876  ig1peu  23931  ig1pdvds  23936  aacjcl  24082  aannenlem2  24084  aannenlem3  24085  aalioulem2  24088  taylfval  24113  radcnvcl  24171  radcnvlt1  24172  radcnvle  24174  abelth  24195  abelth2  24196  pilem2  24206  pilem3  24207  pige3  24269  recosf1o  24281  resinf1o  24282  tanord1  24283  logcn  24393  dvlog  24397  dvlog2lem  24398  efopn  24404  logtayl  24406  cxpcn3  24489  loglesqrt  24499  ssscongptld  24552  leibpi  24669  efrlim  24696  jensenlem1  24713  jensenlem2  24714  jensen  24715  amgm  24717  lgamgulmlem2  24756  ftalem5  24803  efnnfsumcl  24829  efchtdvds  24885  dvdsmulf1o  24920  fsumdvdsmul  24921  lgsfcl2  25028  2sqlem6  25148  2sqlem8  25151  2sqlem9  25152  rpvmasumlem  25176  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem3  25208  dchrisum0  25209  rplogsum  25216  dirith2  25217  axtgcgrrflx  25361  axtgcgrid  25362  axtgsegcon  25363  axtg5seg  25364  axtgbtwnid  25365  axtgpasch  25366  axtgcont1  25367  tgcgr4  25426  motcgrg  25439  tglng  25441  upgrss  25983  pthdivtx  26625  disjxwwlkn  26808  nmlno0lem  27648  hlimcaui  28093  chsspwh  28104  shsss  28172  chintcli  28190  shsleji  28229  shub1i  28233  shsval2i  28246  lejdii  28397  spanuni  28403  sshhococi  28405  spansnpji  28437  osumcori  28502  5oai  28520  3oalem6  28526  3oai  28527  pjssmii  28540  mayete3i  28587  mayetes3i  28588  nmlnop0iALT  28854  imaelshi  28917  pjnmopi  29007  pjclem1  29054  pjci  29059  mdslmd1lem1  29184  shatomistici  29220  hatomistici  29221  chpssati  29222  xppreima  29449  iundisjfi  29555  iundisj2fi  29556  fprodex01  29571  xrsmulgzz  29678  fsumrp0cl  29695  gsummpt2co  29780  xrge0slmod  29844  unitsscn  29942  ordtconnlem1  29970  xrge0iifhom  29983  lmlimxrge0  29994  lmxrge0  29998  indsumin  30084  esumcst  30125  esumpfinvallem  30136  esumpfinval  30137  esumpfinvalf  30138  esumcvg  30148  imambfm  30324  elmbfmvol2  30329  sxbrsigalem3  30334  sxbrsigalem2  30348  sxbrsigalem4  30349  sitgclg  30404  eulerpartlem1  30429  eulerpartlemgvv  30438  eulerpartlemgh  30440  eulerpartlemgf  30441  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemiex  30563  ballotlemsup  30566  ballotlemsdom  30573  ballotlemsima  30577  ballotlemrv2  30583  ballotth  30599  signsplypnf  30627  signsply0  30628  rpsqrtcn  30671  itgexpif  30684  fsum2dsub  30685  reprfi2  30701  chtvalz  30707  breprexplemc  30710  breprexpnat  30712  circlemeth  30718  circlemethnat  30719  circlevma  30720  circlemethhgt  30721  hgt750lemd  30726  hgt750lema  30735  tgoldbachgtde  30738  tgoldbachgtda  30739  tgoldbachgt  30741  bnj1145  31061  bnj1286  31087  subfacp1lem2a  31162  erdszelem4  31176  erdszelem5  31177  erdszelem7  31179  erdszelem8  31180  kur14lem7  31194  kur14lem9  31196  cvxpconn  31224  cvxsconn  31225  resconn  31228  iccllysconn  31232  noextendseq  31820  txpss3v  31985  txprel  31986  limitssson  32018  finminlem  32312  tailf  32370  filnetlem3  32375  onint1  32448  bj-unrab  32922  bj-2upln1upl  33012  bj-rrvecsscmn  33152  taupilem2  33168  taupi  33169  poimirlem3  33412  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  broucube  33443  opnmbllem0  33445  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  mbfposadd  33457  cnambfre  33458  itg2addnc  33464  ftc1cnnclem  33483  ftc1cnnc  33484  ftc1anclem3  33487  ftc1anclem7  33491  ftc1anc  33493  ftc2nc  33494  dvreasin  33498  dvreacos  33499  areacirclem1  33500  areacirclem2  33501  areacirc  33505  caures  33556  reheibor  33638  xrnss3v  34135  xrnrel  34136  atlatmstc  34606  atlatle  34607  pmaple  35047  sspadd1  35101  sspadd2  35102  diophin  37336  4rexfrabdioph  37362  6rexfrabdioph  37363  irrapxlem1  37386  irrapx1  37392  monotuz  37506  jm2.27dlem5  37580  hbtlem2  37694  algbase  37748  algaddg  37749  algmulr  37750  algsca  37751  algvsca  37752  itgpowd  37800  arearect  37801  areaquad  37802  rtrclex  37924  trclubgNEW  37925  trclexi  37927  rtrclexi  37928  cnvtrcl0  37933  dfrtrcl5  37936  trrelsuperrel2dg  37963  relexpaddss  38010  brtrclfv2  38019  frege131d  38056  xphe  38075  idhe  38081  clsk3nimkb  38338  gneispace  38432  k0004val0  38452  lhe4.4ex1a  38528  uzmptshftfval  38545  binomcxplemdvbinom  38552  binomcxplemcvg  38553  binomcxplemnotnn0  38555  relopabVD  39137  fzisoeu  39514  fzsscn  39526  fzssre  39529  fzossuz  39598  fzossz  39599  uzssre  39620  zssxr  39621  uzssre2  39633  supminfxr  39694  uzsscn  39706  rpssxr  39711  ioosscn  39716  uzinico  39787  limcresiooub  39874  limcresioolb  39875  limcleqr  39876  limclner  39883  limclr  39887  limsupequzmpt2  39950  liminfval2  40000  liminfequzmpt2  40023  icccncfext  40100  cncficcgt0  40101  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem1  40161  dvnprodlem2  40162  itgsin0pilem1  40165  itgsinexplem1  40169  itgsinexp  40170  dirkercncflem2  40321  fourierdlem16  40340  fourierdlem18  40342  fourierdlem20  40344  fourierdlem21  40345  fourierdlem22  40346  fourierdlem25  40349  fourierdlem37  40361  fourierdlem42  40366  fourierdlem50  40373  fourierdlem52  40375  fourierdlem62  40385  fourierdlem64  40387  fourierdlem66  40389  fourierdlem68  40391  fourierdlem74  40397  fourierdlem75  40398  fourierdlem76  40399  fourierdlem79  40402  fourierdlem83  40406  fourierdlem95  40418  fourierdlem101  40424  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem24  40475  etransclem48  40499  sge0sn  40596  sge0tsms  40597  sge0f1o  40599  sge0pr  40611  sge0resplit  40623  sge0split  40626  sge0iunmptlemre  40632  sge0isummpt2  40649  carageniuncllem1  40735  hoicvr  40762  hoicvrrex  40770  hoidmvlelem2  40810  hspmbl  40843  smfmullem4  41001  prmdvdsfmtnof1lem1  41496  prmdvdsfmtnof  41498  oddibas  41813  2zrngbas  41936  2zrng0  41938  aacllem  42547  amgmlemALT  42549