MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sstri Structured version   Visualization version   GIF version

Theorem sstri 3597
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
StepHypRef Expression
1 sstri.1 . 2 𝐴𝐵
2 sstri.2 . 2 𝐵𝐶
3 sstr2 3595 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  snsstp1  4322  snsstp2  4323  uniintsn  4486  ssrnres  5541  cossxp  5627  foimacnv  6121  ssimaex  6230  riotassuni  6613  oprabss  6711  dmexg  7059  rnexg  7060  fabexg  7084  fparlem3  7239  fparlem4  7240  snopsuppss  7270  tposssxp  7316  mapsspw  7853  sbthlem5  8034  sbthlem7  8036  cnvimamptfin  8227  marypha1lem  8299  ordtypelem4  8386  hartogslem1  8407  tc2  8578  tz9.12lem1  8610  rankval4  8690  rankxpl  8698  rankmapu  8701  rankxplim  8702  infxpenlem  8796  ackbij1lem18  9019  cflm  9032  fin23lem29  9123  hsmexlem4  9211  hsmexlem5  9212  brdom3  9310  brdom5  9311  brdom4  9312  smobeth  9368  pwfseqlem3  9442  wundm  9510  wunrn  9511  wunex2  9520  ltsopi  9670  dmaddpi  9672  dmmulpi  9673  nqerf  9712  ltrelxr  10059  nnsscn  10985  nn0sscn  11257  uzwo2  11712  infssuzle  11731  infssuzcl  11732  uzwo3  11743  nn0ssq  11756  nnssq  11757  qsscn  11759  rpnnen1lem3  11776  rpnnen1lem5  11778  rpnnen1lem3OLD  11782  rpnnen1lem5OLD  11784  dflt2  11941  fzval2  12287  fzof  12424  fzossnn  12473  fzo0ssnn0OLD  12506  injresinj  12545  flval3  12572  uzsup  12618  uzrdgfni  12713  expcl2lem  12828  rpexpcl  12835  expge0  12852  expge1  12853  hashxrcl  13104  seqcoll  13202  wrdexg  13270  xptrrel  13669  trclublem  13684  sqrlem3  13935  limsupval2  14161  limsupgre  14162  rlimpm  14181  rlimclim  14227  isercolllem1  14345  isercolllem2  14346  isercoll  14348  caurcvg  14357  caucvg  14359  summolem2a  14395  summolem2  14396  zsum  14398  fsumcvg3  14409  fsumrpcl  14417  fsumge0  14473  climfsum  14498  ackbijnn  14504  prodmolem2a  14608  prodmolem2  14609  zprod  14611  fprodrpcl  14630  fprodge0  14668  fprodge1  14670  rprisefaccl  14698  divalglem8  15066  sadaddlem  15131  lcmfval  15277  isprm3  15339  maxprmfct  15364  pclem  15486  prmreclem1  15563  prmreclem2  15564  prmreclem3  15565  1arith  15574  4sqlem11  15602  ramtlecl  15647  ramcl2lem  15656  ramxrcl  15664  prmgaplem3  15700  prmgaplem4  15701  cshwshashlem1  15745  structfn  15816  strlemor1OLD  15909  strleun  15912  srngbase  15949  srngplusg  15950  srngmulr  15951  lmodbase  15958  lmodplusg  15959  lmodsca  15960  ipsbase  15965  ipsaddg  15966  ipsmulr  15967  ipssca  15968  ipsvsca  15969  ipsip  15970  phlbase  15975  phlplusg  15976  phlsca  15977  phlvsca  15978  phlip  15979  odrngbas  16007  odrngplusg  16008  odrngmulr  16009  odrngtset  16010  odrngle  16011  odrngds  16012  prdsval  16055  prdssca  16056  prdsbas  16057  prdsplusg  16058  prdsmulr  16059  prdsvsca  16060  prdsip  16061  prdsle  16062  prdsds  16064  prdstset  16066  prdshom  16067  prdsco  16068  imasbas  16112  imasds  16113  imasplusg  16117  imasmulr  16118  imassca  16119  imasvsca  16120  imasip  16121  imastset  16122  imasle  16123  wunfunc  16499  fullfunc  16506  fthfunc  16507  isfull  16510  isfth  16514  wunnat  16556  dmcoass  16656  catcisolem  16696  catciso  16697  catcoppccl  16698  catcfuccl  16699  catcxpccl  16787  ipobas  17095  ipolerval  17096  ipotset  17097  psdmrn  17147  psss  17154  ledm  17164  lern  17165  dirdm  17174  dirge  17177  mvdco  17805  f1omvdconj  17806  gexex  18196  gsumval3  18248  lssacs  18907  asplss  19269  aspsubrg  19271  psrass1lem  19317  psrbas  19318  psrplusg  19321  psrmulr  19324  psrsca  19329  psrvscafval  19330  psrass1  19345  psrass23l  19348  psrcom  19349  psrass23  19350  psropprmul  19548  coe1mul2  19579  cnfldbas  19690  cnfldadd  19691  cnfldmul  19692  cnfldcj  19693  cnfldtset  19694  cnfldle  19695  cnfldds  19696  cnfldunif  19697  rge0srg  19757  zntoslem  19845  ofco2  20197  toponsspwpw  20666  dmtopon  20667  leordtval2  20956  lmbrf  21004  lmres  21044  fiuncmp  21147  comppfsc  21275  1stckgenlem  21296  kgencn3  21301  ptbasfi  21324  xkoopn  21332  txcnmpt  21367  txkgen  21395  opnfbas  21586  fmfnfmlem4  21701  tsmsxplem1  21896  trust  21973  restutop  21981  nmoffn  22455  nmofval  22458  nmogelb  22460  nmolb  22461  nmof  22463  qtopbas  22503  tgqioo  22543  re2ndc  22544  iitopon  22622  dfii3  22626  iimulcn  22677  cnheiborlem  22693  bndth  22697  lebnumii  22705  reparphti  22737  pcoass  22764  cphsqrtcl  22924  lmmbrf  23000  iscauf  23018  caucfil  23021  lmclimf  23042  rrxmval  23128  rrxmet  23131  ovolfioo  23176  ovolficc  23177  ovolficcss  23178  ovolfsf  23180  ovollb  23187  ovolicc2lem3  23227  ovolicc2lem4  23228  ovolicc2  23230  volf  23237  volsup  23264  ovolfs2  23279  uniiccdif  23286  uniioovol  23287  uniiccvol  23288  uniioombllem2  23291  uniioombllem3a  23292  uniioombllem3  23293  uniioombllem4  23294  uniioombllem5  23295  uniioombl  23297  dyadmbllem  23307  dyadmbl  23308  opnmbllem  23309  opnmblALT  23311  volsup2  23313  vitalilem4  23320  vitalilem5  23321  vitali  23322  mbfimaopnlem  23362  mbflimsup  23373  i1f0  23394  i1f1  23397  itg11  23398  itg2mulc  23454  itg2gt0  23467  ellimc2  23581  limcresi  23589  dvreslem  23613  dvres2lem  23614  dvaddbr  23641  dvmulbr  23642  dvlipcn  23695  c1liplem1  23697  lhop1lem  23714  lhop1  23715  lhop2  23716  lhop  23717  dvfsumrlim  23732  ftc1cn  23744  itgsubstlem  23749  itgsubst  23750  mdegleb  23762  mdeglt  23763  mdegldg  23764  mdegxrcl  23765  mdegcl  23767  mdegaddle  23772  mdegmullem  23776  deg1mul3le  23814  ig1peu  23869  ig1pdvds  23874  aacjcl  24020  aannenlem2  24022  aannenlem3  24023  aalioulem2  24026  taylfval  24051  radcnvcl  24109  radcnvlt1  24110  radcnvle  24112  abelth  24133  abelth2  24134  pilem2  24144  pilem3  24145  pige3  24207  recosf1o  24219  resinf1o  24220  tanord1  24221  logcn  24327  dvlog  24331  dvlog2lem  24332  efopn  24338  logtayl  24340  cxpcn3  24423  loglesqrt  24433  ssscongptld  24486  leibpi  24603  efrlim  24630  jensenlem1  24647  jensenlem2  24648  jensen  24649  amgm  24651  lgamgulmlem2  24690  ftalem5  24737  efnnfsumcl  24763  efchtdvds  24819  dvdsmulf1o  24854  fsumdvdsmul  24855  lgsfcl2  24962  2sqlem6  25082  2sqlem8  25085  2sqlem9  25086  rpvmasumlem  25110  rpvmasum2  25135  dchrisum0re  25136  dchrisum0lem3  25142  dchrisum0  25143  rplogsum  25150  dirith2  25151  axtgcgrrflx  25295  axtgcgrid  25296  axtgsegcon  25297  axtg5seg  25298  axtgbtwnid  25299  axtgpasch  25300  axtgcont1  25301  tgcgr4  25360  motcgrg  25373  tglng  25375  upgrss  25913  pthdivtx  26528  disjxwwlkn  26711  nmlno0lem  27536  hlimcaui  27981  chsspwh  27992  shsss  28060  chintcli  28078  shsleji  28117  shub1i  28121  shsval2i  28134  lejdii  28285  spanuni  28291  sshhococi  28293  spansnpji  28325  osumcori  28390  5oai  28408  3oalem6  28414  3oai  28415  pjssmii  28428  mayete3i  28475  mayetes3i  28476  nmlnop0iALT  28742  imaelshi  28805  pjnmopi  28895  pjclem1  28942  pjci  28947  mdslmd1lem1  29072  shatomistici  29108  hatomistici  29109  chpssati  29110  xppreima  29332  iundisjfi  29438  iundisj2fi  29439  xrsmulgzz  29505  fsumrp0cl  29522  gsummpt2co  29607  xrge0slmod  29671  unitsscn  29766  ordtconnlem1  29794  xrge0iifhom  29807  lmlimxrge0  29818  lmxrge0  29822  esumcst  29948  esumpfinvallem  29959  esumpfinval  29960  esumpfinvalf  29961  esumcvg  29971  imambfm  30147  elmbfmvol2  30152  sxbrsigalem3  30157  sxbrsigalem2  30171  sxbrsigalem4  30172  sitgclg  30227  eulerpartlem1  30252  eulerpartlemgvv  30261  eulerpartlemgh  30263  eulerpartlemgf  30264  ballotlemfc0  30377  ballotlemfcc  30378  ballotlemiex  30386  ballotlemsup  30389  ballotlemsdom  30396  ballotlemsima  30400  ballotlemrv2  30406  ballotth  30422  signsplypnf  30449  signsply0  30450  itgexpif  30493  breprsuc  30501  bnj1145  30822  bnj1286  30848  subfacp1lem2a  30923  erdszelem4  30937  erdszelem5  30938  erdszelem7  30940  erdszelem8  30941  kur14lem7  30955  kur14lem9  30957  cvxpconn  30985  cvxsconn  30986  resconn  30989  iccllysconn  30993  txpss3v  31680  txprel  31681  limitssson  31713  finminlem  32007  tailf  32065  filnetlem3  32070  onint1  32143  bj-unrab  32622  bj-2upln1upl  32712  bj-rrvecsscmn  32824  taupilem2  32840  taupi  32841  poimirlem3  33083  poimirlem30  33110  poimirlem31  33111  poimirlem32  33112  broucube  33114  opnmbllem0  33116  mblfinlem1  33117  mblfinlem2  33118  mblfinlem3  33119  mblfinlem4  33120  ismblfin  33121  mbfposadd  33128  cnambfre  33129  itg2addnc  33135  ftc1cnnclem  33154  ftc1cnnc  33155  ftc1anclem3  33158  ftc1anclem7  33162  ftc1anc  33164  ftc2nc  33165  dvreasin  33169  dvreacos  33170  areacirclem1  33171  areacirclem2  33172  areacirc  33176  caures  33227  reheibor  33309  atlatmstc  34125  atlatle  34126  pmaple  34566  sspadd1  34620  sspadd2  34621  diophin  36855  4rexfrabdioph  36881  6rexfrabdioph  36882  irrapxlem1  36905  irrapx1  36911  monotuz  37025  jm2.27dlem5  37099  hbtlem2  37214  algbase  37268  algaddg  37269  algmulr  37270  algsca  37271  algvsca  37272  itgpowd  37320  arearect  37321  areaquad  37322  rtrclex  37444  trclubgNEW  37445  trclexi  37447  rtrclexi  37448  cnvtrcl0  37453  dfrtrcl5  37456  trrelsuperrel2dg  37483  relexpaddss  37530  brtrclfv2  37539  frege131d  37576  xphe  37596  idhe  37602  clsk3nimkb  37859  gneispace  37953  k0004val0  37973  lhe4.4ex1a  38049  uzmptshftfval  38066  binomcxplemdvbinom  38073  binomcxplemcvg  38074  binomcxplemnotnn0  38076  relopabVD  38659  fzisoeu  39013  fzsscn  39025  fzssre  39028  fzossuz  39097  fzossz  39098  uzssre  39119  zssxr  39120  uzssre2  39132  ioosscn  39162  uzinico  39233  limcresiooub  39310  limcresioolb  39311  limcleqr  39312  limclner  39319  limclr  39323  limsupequzmpt2  39386  icccncfext  39435  cncficcgt0  39436  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvnprodlem1  39498  dvnprodlem2  39499  itgsin0pilem1  39502  itgsinexplem1  39506  itgsinexp  39507  dirkercncflem2  39658  fourierdlem16  39677  fourierdlem18  39679  fourierdlem20  39681  fourierdlem21  39682  fourierdlem22  39683  fourierdlem25  39686  fourierdlem37  39698  fourierdlem42  39703  fourierdlem50  39710  fourierdlem52  39712  fourierdlem62  39722  fourierdlem64  39724  fourierdlem66  39726  fourierdlem68  39728  fourierdlem74  39734  fourierdlem75  39735  fourierdlem76  39736  fourierdlem79  39739  fourierdlem83  39743  fourierdlem95  39755  fourierdlem101  39761  fourierdlem102  39762  fourierdlem103  39763  fourierdlem104  39764  fourierdlem112  39772  fourierdlem114  39774  sqwvfoura  39782  sqwvfourb  39783  fouriersw  39785  etransclem24  39812  etransclem48  39836  sge0sn  39933  sge0tsms  39934  sge0f1o  39936  sge0pr  39948  sge0resplit  39960  sge0split  39963  sge0iunmptlemre  39969  sge0isummpt2  39986  carageniuncllem1  40072  hoicvr  40099  hoicvrrex  40107  hoidmvlelem2  40147  hspmbl  40180  smfmullem4  40338  prmdvdsfmtnof1lem1  40825  prmdvdsfmtnof  40827  oddibas  41131  2zrngbas  41254  2zrng0  41256  aacllem  41880  amgmlemALT  41882
  Copyright terms: Public domain W3C validator