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

Theorem sstri 3604
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 3602 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  snsstp1  4338  snsstp2  4339  uniintsn  4505  ssrnres  5560  cossxp  5646  foimacnv  6141  ssimaex  6250  riotassuni  6633  oprabss  6731  dmexg  7082  rnexg  7083  fabexg  7107  fparlem3  7264  fparlem4  7265  snopsuppss  7295  tposssxp  7341  mapsspw  7878  sbthlem5  8059  sbthlem7  8061  cnvimamptfin  8252  marypha1lem  8324  ordtypelem4  8411  hartogslem1  8432  tc2  8603  tz9.12lem1  8635  rankval4  8715  rankxpl  8723  rankmapu  8726  rankxplim  8727  infxpenlem  8821  ackbij1lem18  9044  cflm  9057  fin23lem29  9148  hsmexlem4  9236  hsmexlem5  9237  brdom3  9335  brdom5  9336  brdom4  9337  smobeth  9393  pwfseqlem3  9467  wundm  9535  wunrn  9536  wunex2  9545  ltsopi  9695  dmaddpi  9697  dmmulpi  9698  nqerf  9737  ltrelxr  10084  nnsscn  11010  nn0sscn  11282  uzwo2  11737  infssuzle  11756  infssuzcl  11757  uzwo3  11768  nn0ssq  11781  nnssq  11782  qsscn  11784  rpnnen1lem3  11801  rpnnen1lem5  11803  rpnnen1lem3OLD  11807  rpnnen1lem5OLD  11809  dflt2  11966  fzval2  12314  fzof  12451  fzossnn  12500  fzo0ssnn0OLD  12533  injresinj  12572  flval3  12599  uzsup  12645  uzrdgfni  12740  expcl2lem  12855  rpexpcl  12862  expge0  12879  expge1  12880  hashxrcl  13131  seqcoll  13231  wrdexg  13298  xptrrel  13700  trclublem  13715  sqrlem3  13966  limsupval2  14192  limsupgre  14193  rlimpm  14212  rlimclim  14258  isercolllem1  14376  isercolllem2  14377  isercoll  14379  caurcvg  14388  caucvg  14390  summolem2a  14427  summolem2  14428  zsum  14430  fsumcvg3  14441  fsumrpcl  14449  fsumge0  14508  climfsum  14533  ackbijnn  14541  prodmolem2a  14645  prodmolem2  14646  zprod  14648  fprodrpcl  14667  fprodge0  14705  fprodge1  14707  rprisefaccl  14735  divalglem8  15104  sadaddlem  15169  lcmfval  15315  isprm3  15377  maxprmfct  15402  pclem  15524  prmreclem1  15601  prmreclem2  15602  prmreclem3  15603  1arith  15612  4sqlem11  15640  ramtlecl  15685  ramcl2lem  15694  ramxrcl  15702  prmgaplem3  15738  prmgaplem4  15739  cshwshashlem1  15783  structfn  15855  strlemor1OLD  15950  strleun  15953  srngbase  15990  srngplusg  15991  srngmulr  15992  lmodbase  15999  lmodplusg  16000  lmodsca  16001  ipsbase  16006  ipsaddg  16007  ipsmulr  16008  ipssca  16009  ipsvsca  16010  ipsip  16011  phlbase  16016  phlplusg  16017  phlsca  16018  phlvsca  16019  phlip  16020  odrngbas  16048  odrngplusg  16049  odrngmulr  16050  odrngtset  16051  odrngle  16052  odrngds  16053  prdsval  16096  prdssca  16097  prdsbas  16098  prdsplusg  16099  prdsmulr  16100  prdsvsca  16101  prdsip  16102  prdsle  16103  prdsds  16105  prdstset  16107  prdshom  16108  prdsco  16109  imasbas  16153  imasds  16154  imasplusg  16158  imasmulr  16159  imassca  16160  imasvsca  16161  imasip  16162  imastset  16163  imasle  16164  wunfunc  16540  fullfunc  16547  fthfunc  16548  isfull  16551  isfth  16555  wunnat  16597  dmcoass  16697  catcisolem  16737  catciso  16738  catcoppccl  16739  catcfuccl  16740  catcxpccl  16828  ipobas  17136  ipolerval  17137  ipotset  17138  psdmrn  17188  psss  17195  ledm  17205  lern  17206  dirdm  17215  dirge  17218  mvdco  17846  f1omvdconj  17847  gexex  18237  gsumval3  18289  lssacs  18948  asplss  19310  aspsubrg  19312  psrass1lem  19358  psrbas  19359  psrplusg  19362  psrmulr  19365  psrsca  19370  psrvscafval  19371  psrass1  19386  psrass23l  19389  psrcom  19390  psrass23  19391  psropprmul  19589  coe1mul2  19620  cnfldbas  19731  cnfldadd  19732  cnfldmul  19733  cnfldcj  19734  cnfldtset  19735  cnfldle  19736  cnfldds  19737  cnfldunif  19738  rge0srg  19798  zntoslem  19886  ofco2  20238  toponsspwpw  20707  dmtopon  20708  leordtval2  20997  lmbrf  21045  lmres  21085  fiuncmp  21188  comppfsc  21316  1stckgenlem  21337  kgencn3  21342  ptbasfi  21365  xkoopn  21373  txcnmpt  21408  txkgen  21436  opnfbas  21627  fmfnfmlem4  21742  tsmsxplem1  21937  trust  22014  restutop  22022  nmoffn  22496  nmofval  22499  nmogelb  22501  nmolb  22502  nmof  22504  qtopbas  22544  tgqioo  22584  re2ndc  22585  iitopon  22663  dfii3  22667  iimulcn  22718  cnheiborlem  22734  bndth  22738  lebnumii  22746  reparphti  22778  pcoass  22805  cphsqrtcl  22965  lmmbrf  23041  iscauf  23059  caucfil  23062  lmclimf  23083  rrxmval  23169  rrxmet  23172  ovolfioo  23217  ovolficc  23218  ovolficcss  23219  ovolfsf  23221  ovollb  23228  ovolicc2lem3  23268  ovolicc2lem4  23269  ovolicc2  23271  volf  23278  volsup  23305  ovolfs2  23320  uniiccdif  23327  uniioovol  23328  uniiccvol  23329  uniioombllem2  23332  uniioombllem3a  23333  uniioombllem3  23334  uniioombllem4  23335  uniioombllem5  23336  uniioombl  23338  dyadmbllem  23348  dyadmbl  23349  opnmbllem  23350  opnmblALT  23352  volsup2  23354  vitalilem4  23361  vitalilem5  23362  vitali  23363  mbfimaopnlem  23403  mbflimsup  23414  i1f0  23435  i1f1  23438  itg11  23439  itg2mulc  23495  itg2gt0  23508  ellimc2  23622  limcresi  23630  dvreslem  23654  dvres2lem  23655  dvaddbr  23682  dvmulbr  23683  dvlipcn  23738  c1liplem1  23740  lhop1lem  23757  lhop1  23758  lhop2  23759  lhop  23760  dvfsumrlim  23775  ftc1cn  23787  itgsubstlem  23792  itgsubst  23793  mdegleb  23805  mdeglt  23806  mdegldg  23807  mdegxrcl  23808  mdegcl  23810  mdegaddle  23815  mdegmullem  23819  deg1mul3le  23857  ig1peu  23912  ig1pdvds  23917  aacjcl  24063  aannenlem2  24065  aannenlem3  24066  aalioulem2  24069  taylfval  24094  radcnvcl  24152  radcnvlt1  24153  radcnvle  24155  abelth  24176  abelth2  24177  pilem2  24187  pilem3  24188  pige3  24250  recosf1o  24262  resinf1o  24263  tanord1  24264  logcn  24374  dvlog  24378  dvlog2lem  24379  efopn  24385  logtayl  24387  cxpcn3  24470  loglesqrt  24480  ssscongptld  24533  leibpi  24650  efrlim  24677  jensenlem1  24694  jensenlem2  24695  jensen  24696  amgm  24698  lgamgulmlem2  24737  ftalem5  24784  efnnfsumcl  24810  efchtdvds  24866  dvdsmulf1o  24901  fsumdvdsmul  24902  lgsfcl2  25009  2sqlem6  25129  2sqlem8  25132  2sqlem9  25133  rpvmasumlem  25157  rpvmasum2  25182  dchrisum0re  25183  dchrisum0lem3  25189  dchrisum0  25190  rplogsum  25197  dirith2  25198  axtgcgrrflx  25342  axtgcgrid  25343  axtgsegcon  25344  axtg5seg  25345  axtgbtwnid  25346  axtgpasch  25347  axtgcont1  25348  tgcgr4  25407  motcgrg  25420  tglng  25422  upgrss  25964  pthdivtx  26606  disjxwwlkn  26789  nmlno0lem  27618  hlimcaui  28063  chsspwh  28074  shsss  28142  chintcli  28160  shsleji  28199  shub1i  28203  shsval2i  28216  lejdii  28367  spanuni  28373  sshhococi  28375  spansnpji  28407  osumcori  28472  5oai  28490  3oalem6  28496  3oai  28497  pjssmii  28510  mayete3i  28557  mayetes3i  28558  nmlnop0iALT  28824  imaelshi  28887  pjnmopi  28977  pjclem1  29024  pjci  29029  mdslmd1lem1  29154  shatomistici  29190  hatomistici  29191  chpssati  29192  xppreima  29422  iundisjfi  29529  iundisj2fi  29530  fprodex01  29545  xrsmulgzz  29652  fsumrp0cl  29669  gsummpt2co  29754  xrge0slmod  29818  unitsscn  29916  ordtconnlem1  29944  xrge0iifhom  29957  lmlimxrge0  29968  lmxrge0  29972  indsumin  30058  esumcst  30099  esumpfinvallem  30110  esumpfinval  30111  esumpfinvalf  30112  esumcvg  30122  imambfm  30298  elmbfmvol2  30303  sxbrsigalem3  30308  sxbrsigalem2  30322  sxbrsigalem4  30323  sitgclg  30378  eulerpartlem1  30403  eulerpartlemgvv  30412  eulerpartlemgh  30414  eulerpartlemgf  30415  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemiex  30537  ballotlemsup  30540  ballotlemsdom  30547  ballotlemsima  30551  ballotlemrv2  30557  ballotth  30573  signsplypnf  30601  signsply0  30602  rpsqrtcn  30645  itgexpif  30658  fsum2dsub  30659  reprfi2  30675  chtvalz  30681  breprexplemc  30684  breprexpnat  30686  circlemeth  30692  circlemethnat  30693  circlevma  30694  circlemethhgt  30695  hgt750lemd  30700  hgt750lema  30709  tgoldbachgtde  30712  tgoldbachgtda  30713  tgoldbachgt  30715  bnj1145  31035  bnj1286  31061  subfacp1lem2a  31136  erdszelem4  31150  erdszelem5  31151  erdszelem7  31153  erdszelem8  31154  kur14lem7  31168  kur14lem9  31170  cvxpconn  31198  cvxsconn  31199  resconn  31202  iccllysconn  31206  noextendseq  31794  txpss3v  31960  txprel  31961  limitssson  31993  finminlem  32287  tailf  32345  filnetlem3  32350  onint1  32423  bj-unrab  32897  bj-2upln1upl  32987  bj-rrvecsscmn  33123  taupilem2  33139  taupi  33140  poimirlem3  33383  poimirlem30  33410  poimirlem31  33411  poimirlem32  33412  broucube  33414  opnmbllem0  33416  mblfinlem1  33417  mblfinlem2  33418  mblfinlem3  33419  mblfinlem4  33420  ismblfin  33421  mbfposadd  33428  cnambfre  33429  itg2addnc  33435  ftc1cnnclem  33454  ftc1cnnc  33455  ftc1anclem3  33458  ftc1anclem7  33462  ftc1anc  33464  ftc2nc  33465  dvreasin  33469  dvreacos  33470  areacirclem1  33471  areacirclem2  33472  areacirc  33476  caures  33527  reheibor  33609  atlatmstc  34425  atlatle  34426  pmaple  34866  sspadd1  34920  sspadd2  34921  diophin  37155  4rexfrabdioph  37181  6rexfrabdioph  37182  irrapxlem1  37205  irrapx1  37211  monotuz  37325  jm2.27dlem5  37399  hbtlem2  37513  algbase  37567  algaddg  37568  algmulr  37569  algsca  37570  algvsca  37571  itgpowd  37619  arearect  37620  areaquad  37621  rtrclex  37743  trclubgNEW  37744  trclexi  37746  rtrclexi  37747  cnvtrcl0  37752  dfrtrcl5  37755  trrelsuperrel2dg  37782  relexpaddss  37829  brtrclfv2  37838  frege131d  37875  xphe  37895  idhe  37901  clsk3nimkb  38158  gneispace  38252  k0004val0  38272  lhe4.4ex1a  38348  uzmptshftfval  38365  binomcxplemdvbinom  38372  binomcxplemcvg  38373  binomcxplemnotnn0  38375  relopabVD  38957  fzisoeu  39327  fzsscn  39339  fzssre  39342  fzossuz  39411  fzossz  39412  uzssre  39433  zssxr  39434  uzssre2  39446  supminfxr  39507  ioosscn  39519  uzinico  39590  limcresiooub  39674  limcresioolb  39675  limcleqr  39676  limclner  39683  limclr  39687  limsupequzmpt2  39750  liminfval2  39794  liminfequzmpt2  39817  icccncfext  39863  cncficcgt0  39864  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  dvnprodlem1  39924  dvnprodlem2  39925  itgsin0pilem1  39928  itgsinexplem1  39932  itgsinexp  39933  dirkercncflem2  40084  fourierdlem16  40103  fourierdlem18  40105  fourierdlem20  40107  fourierdlem21  40108  fourierdlem22  40109  fourierdlem25  40112  fourierdlem37  40124  fourierdlem42  40129  fourierdlem50  40136  fourierdlem52  40138  fourierdlem62  40148  fourierdlem64  40150  fourierdlem66  40152  fourierdlem68  40154  fourierdlem74  40160  fourierdlem75  40161  fourierdlem76  40162  fourierdlem79  40165  fourierdlem83  40169  fourierdlem95  40181  fourierdlem101  40187  fourierdlem102  40188  fourierdlem103  40189  fourierdlem104  40190  fourierdlem112  40198  fourierdlem114  40200  sqwvfoura  40208  sqwvfourb  40209  fouriersw  40211  etransclem24  40238  etransclem48  40262  sge0sn  40359  sge0tsms  40360  sge0f1o  40362  sge0pr  40374  sge0resplit  40386  sge0split  40389  sge0iunmptlemre  40395  sge0isummpt2  40412  carageniuncllem1  40498  hoicvr  40525  hoicvrrex  40533  hoidmvlelem2  40573  hspmbl  40606  smfmullem4  40764  prmdvdsfmtnof1lem1  41261  prmdvdsfmtnof  41263  oddibas  41578  2zrngbas  41701  2zrng0  41703  aacllem  42312  amgmlemALT  42314
  Copyright terms: Public domain W3C validator