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

Theorem sstri 3573
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 3571 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-in 3543  df-ss 3550
This theorem is referenced by:  snsstp1  4283  snsstp2  4284  uniintsn  4440  ssrnres  5474  cossxp  5558  foimacnv  6049  ssimaex  6155  riotassuni  6522  oprabss  6619  dmexg  6963  rnexg  6964  fabexg  6989  fparlem3  7140  fparlem4  7141  snopsuppss  7171  tposssxp  7217  mapsspw  7753  sbthlem5  7933  sbthlem7  7935  cnvimamptfin  8124  marypha1lem  8196  ordtypelem4  8283  hartogslem1  8304  tc2  8475  tz9.12lem1  8507  rankval4  8587  rankxpl  8595  rankmapu  8598  rankxplim  8599  infxpenlem  8693  ackbij1lem18  8916  cflm  8929  fin23lem29  9020  hsmexlem4  9108  hsmexlem5  9109  brdom3  9205  brdom5  9206  brdom4  9207  smobeth  9261  pwfseqlem3  9335  wundm  9403  wunrn  9404  wunex2  9413  ltsopi  9563  dmaddpi  9565  dmmulpi  9566  nqerf  9605  ltrelxr  9947  nnsscn  10869  nn0sscn  11141  uzwo2  11581  infssuzle  11600  infssuzcl  11601  uzwo3  11612  nn0ssq  11625  nnssq  11626  qsscn  11628  rpnnen1lem3  11645  rpnnen1lem5  11647  rpnnen1lem3OLD  11651  rpnnen1lem5OLD  11653  dflt2  11813  fzval2  12152  fzof  12288  fzossnn  12336  fzo0ssnn0OLD  12368  injresinj  12403  flval3  12430  uzsup  12476  uzrdgfni  12571  expcl2lem  12686  rpexpcl  12693  expge0  12710  expge1  12711  hashxrcl  12959  seqcoll  13054  wrdexg  13113  xptrrel  13510  trclublem  13525  sqrlem3  13776  limsupval2  14002  limsupgre  14003  rlimpm  14022  rlimclim  14068  isercolllem1  14186  isercolllem2  14187  isercoll  14189  caurcvg  14198  caucvg  14200  summolem2a  14236  summolem2  14237  zsum  14239  fsumcvg3  14250  fsumrpcl  14258  fsumge0  14311  climfsum  14336  ackbijnn  14342  prodmolem2a  14446  prodmolem2  14447  zprod  14449  fprodrpcl  14468  fprodge0  14506  fprodge1  14508  rprisefaccl  14536  divalglem8  14904  sadaddlem  14969  lcmfval  15115  isprm3  15177  maxprmfct  15202  pclem  15324  prmreclem1  15401  prmreclem2  15402  prmreclem3  15403  1arith  15412  4sqlem11  15440  ramtlecl  15485  ramcl2lem  15494  ramxrcl  15502  prmgaplem3  15538  prmgaplem4  15539  cshwshashlem1  15583  structfn  15651  strlemor1  15739  strleun  15742  srngbase  15775  srngplusg  15776  srngmulr  15777  lmodbase  15784  lmodplusg  15785  lmodsca  15786  ipsbase  15791  ipsaddg  15792  ipsmulr  15793  ipssca  15794  ipsvsca  15795  ipsip  15796  phlbase  15801  phlplusg  15802  phlsca  15803  phlvsca  15804  phlip  15805  odrngbas  15833  odrngplusg  15834  odrngmulr  15835  odrngtset  15836  odrngle  15837  odrngds  15838  prdsval  15881  prdssca  15882  prdsbas  15883  prdsplusg  15884  prdsmulr  15885  prdsvsca  15886  prdsip  15887  prdsle  15888  prdsds  15890  prdstset  15892  prdshom  15893  prdsco  15894  imasbas  15938  imasds  15939  imasplusg  15943  imasmulr  15944  imassca  15945  imasvsca  15946  imasip  15947  imastset  15948  imasle  15949  wunfunc  16325  fullfunc  16332  fthfunc  16333  isfull  16336  isfth  16340  wunnat  16382  dmcoass  16482  catcisolem  16522  catciso  16523  catcoppccl  16524  catcfuccl  16525  catcxpccl  16613  ipobas  16921  ipolerval  16922  ipotset  16923  psdmrn  16973  psss  16980  ledm  16990  lern  16991  dirdm  17000  dirge  17003  mvdco  17631  f1omvdconj  17632  gexex  18022  gsumval3  18074  lssacs  18731  asplss  19093  aspsubrg  19095  psrass1lem  19141  psrbas  19142  psrplusg  19145  psrmulr  19148  psrsca  19153  psrvscafval  19154  psrass1  19169  psrass23l  19172  psrcom  19173  psrass23  19174  psropprmul  19372  coe1mul2  19403  cnfldbas  19514  cnfldadd  19515  cnfldmul  19516  cnfldcj  19517  cnfldtset  19518  cnfldle  19519  cnfldds  19520  cnfldunif  19521  rge0srg  19579  zntoslem  19666  ofco2  20015  leordtval2  20765  lmbrf  20813  lmres  20853  fiuncmp  20956  comppfsc  21084  1stckgenlem  21105  kgencn3  21110  ptbasfi  21133  xkoopn  21141  txcnmpt  21176  txkgen  21204  opnfbas  21395  fmfnfmlem4  21510  tsmsxplem1  21705  trust  21782  restutop  21790  nmoffn  22254  nmofval  22257  nmogelb  22259  nmolb  22260  nmof  22262  qtopbas  22302  tgqioo  22340  re2ndc  22341  iitopon  22418  dfii3  22422  iimulcn  22473  cnheiborlem  22489  bndth  22493  lebnumii  22501  reparphti  22533  pcoass  22560  cphsqrtcl  22713  lmmbrf  22783  iscauf  22801  caucfil  22804  lmclimf  22824  rrxmval  22910  rrxmet  22913  ovolfioo  22957  ovolficc  22958  ovolficcss  22959  ovolfsf  22961  ovollb  22968  ovolicc2lem3  23008  ovolicc2lem4  23009  ovolicc2  23011  volf  23018  volsup  23045  ovolfs2  23059  uniiccdif  23066  uniioovol  23067  uniiccvol  23068  uniioombllem2  23071  uniioombllem3a  23072  uniioombllem3  23073  uniioombllem4  23074  uniioombllem5  23075  uniioombl  23077  dyadmbllem  23087  dyadmbl  23088  opnmbllem  23089  opnmblALT  23091  volsup2  23093  vitalilem4  23100  vitalilem5  23101  vitali  23102  mbfimaopnlem  23142  mbflimsup  23153  i1f0  23174  i1f1  23177  itg11  23178  itg2mulc  23234  itg2gt0  23247  ellimc2  23361  limcresi  23369  dvreslem  23393  dvres2lem  23394  dvaddbr  23421  dvmulbr  23422  dvlipcn  23475  c1liplem1  23477  lhop1lem  23494  lhop1  23495  lhop2  23496  lhop  23497  dvfsumrlim  23512  ftc1cn  23524  itgsubstlem  23529  itgsubst  23530  mdegleb  23542  mdeglt  23543  mdegldg  23544  mdegxrcl  23545  mdegcl  23547  mdegaddle  23552  mdegmullem  23556  deg1mul3le  23594  ig1peu  23649  ig1pdvds  23654  aacjcl  23800  aannenlem2  23802  aannenlem3  23803  aalioulem2  23806  taylfval  23831  radcnvcl  23889  radcnvlt1  23890  radcnvle  23892  abelth  23913  abelth2  23914  pilem2  23924  pilem3  23925  pige3  23987  recosf1o  23999  resinf1o  24000  tanord1  24001  logcn  24107  dvlog  24111  dvlog2lem  24112  efopn  24118  logtayl  24120  cxpcn3  24203  loglesqrt  24213  ssscongptld  24266  leibpi  24383  efrlim  24410  jensenlem1  24427  jensenlem2  24428  jensen  24429  amgm  24431  lgamgulmlem2  24470  ftalem5  24517  efnnfsumcl  24543  efchtdvds  24599  dvdsmulf1o  24634  fsumdvdsmul  24635  lgsfcl2  24742  2sqlem6  24862  2sqlem8  24865  2sqlem9  24866  rpvmasumlem  24890  rpvmasum2  24915  dchrisum0re  24916  dchrisum0lem3  24922  dchrisum0  24923  rplogsum  24930  dirith2  24931  axtgcgrrflx  25075  axtgcgrid  25076  axtgsegcon  25077  axtg5seg  25078  axtgbtwnid  25079  axtgpasch  25080  axtgcont1  25081  tgcgr4  25141  motcgrg  25154  tglng  25156  umgrass  25611  constr3pthlem1  25946  disjxwwlkn  26036  nmlno0lem  26835  hlimcaui  27280  chsspwh  27291  shsss  27359  chintcli  27377  shsleji  27416  shub1i  27420  shsval2i  27433  lejdii  27584  spanuni  27590  sshhococi  27592  spansnpji  27624  osumcori  27689  5oai  27707  3oalem6  27713  3oai  27714  pjssmii  27727  mayete3i  27774  mayetes3i  27775  nmlnop0iALT  28041  imaelshi  28104  pjnmopi  28194  pjclem1  28241  pjci  28246  mdslmd1lem1  28371  shatomistici  28407  hatomistici  28408  chpssati  28409  xppreima  28632  iundisjfi  28745  iundisj2fi  28746  xrsmulgzz  28812  fsumrp0cl  28829  gsummpt2co  28914  xrge0slmod  28978  unitsscn  29073  ordtconlem1  29101  xrge0iifhom  29114  lmlimxrge0  29125  lmxrge0  29129  esumcst  29255  esumpfinvallem  29266  esumpfinval  29267  esumpfinvalf  29268  esumcvg  29278  imambfm  29454  elmbfmvol2  29459  sxbrsigalem3  29464  sxbrsigalem2  29478  sxbrsigalem4  29479  sitgclg  29534  eulerpartlem1  29559  eulerpartlemgvv  29568  eulerpartlemgh  29570  eulerpartlemgf  29571  ballotlemfc0  29684  ballotlemfcc  29685  ballotlemiex  29693  ballotlemsup  29696  ballotlemsdom  29703  ballotlemsima  29707  ballotlemrv2  29713  ballotth  29729  signsplypnf  29756  signsply0  29757  bnj1145  30118  bnj1286  30144  subfacp1lem2a  30219  erdszelem4  30233  erdszelem5  30234  erdszelem7  30236  erdszelem8  30237  kur14lem7  30251  kur14lem9  30253  cvxpcon  30281  cvxscon  30282  rescon  30285  iccllyscon  30289  txpss3v  30958  txprel  30959  limitssson  30991  finminlem  31285  tailf  31343  filnetlem3  31348  onint1  31421  bj-unrab  31914  bj-2upln1upl  32005  bj-toponss  32041  bj-dmtopon  32042  bj-rrvecsscmn  32129  taupilem2  32145  taupi  32146  poimirlem3  32382  poimirlem30  32409  poimirlem31  32410  poimirlem32  32411  broucube  32413  opnmbllem0  32415  mblfinlem1  32416  mblfinlem2  32417  mblfinlem3  32418  mblfinlem4  32419  ismblfin  32420  mbfposadd  32427  cnambfre  32428  itg2addnc  32434  ftc1cnnclem  32453  ftc1cnnc  32454  ftc1anclem3  32457  ftc1anclem7  32461  ftc1anc  32463  ftc2nc  32464  dvreasin  32468  dvreacos  32469  areacirclem1  32470  areacirclem2  32471  areacirc  32475  caures  32526  reheibor  32608  atlatmstc  33424  atlatle  33425  pmaple  33865  sspadd1  33919  sspadd2  33920  diophin  36154  4rexfrabdioph  36180  6rexfrabdioph  36181  irrapxlem1  36204  irrapx1  36210  monotuz  36324  jm2.27dlem5  36398  hbtlem2  36513  algbase  36567  algaddg  36568  algmulr  36569  algsca  36570  algvsca  36571  itgpowd  36619  arearect  36620  areaquad  36621  rtrclex  36743  trclubgNEW  36744  trclexi  36746  rtrclexi  36747  cnvtrcl0  36752  dfrtrcl5  36755  trrelsuperrel2dg  36782  relexpaddss  36829  brtrclfv2  36838  frege131d  36875  xphe  36895  idhe  36901  clsk3nimkb  37158  gneispace  37252  k0004val0  37272  lhe4.4ex1a  37350  uzmptshftfval  37367  binomcxplemdvbinom  37374  binomcxplemcvg  37375  binomcxplemnotnn0  37377  relopabVD  37959  fzisoeu  38255  fzsscn  38268  fzssre  38271  fzossuz  38340  fzossz  38341  ioosscn  38364  limcresiooub  38510  limcresioolb  38511  limcleqr  38512  limclner  38519  limclr  38523  icccncfext  38574  cncficcgt0  38575  ioodvbdlimc1lem2  38623  ioodvbdlimc2lem  38625  dvnprodlem1  38637  dvnprodlem2  38638  itgsin0pilem1  38642  itgsinexplem1  38646  itgsinexp  38647  dirkercncflem2  38798  fourierdlem16  38817  fourierdlem18  38819  fourierdlem20  38821  fourierdlem21  38822  fourierdlem22  38823  fourierdlem25  38826  fourierdlem37  38838  fourierdlem42  38843  fourierdlem50  38850  fourierdlem52  38852  fourierdlem62  38862  fourierdlem64  38864  fourierdlem66  38866  fourierdlem68  38868  fourierdlem74  38874  fourierdlem75  38875  fourierdlem76  38876  fourierdlem79  38879  fourierdlem83  38883  fourierdlem95  38895  fourierdlem101  38901  fourierdlem102  38902  fourierdlem103  38903  fourierdlem104  38904  fourierdlem112  38912  fourierdlem114  38914  sqwvfoura  38922  sqwvfourb  38923  fouriersw  38925  etransclem24  38952  etransclem48  38976  sge0sn  39073  sge0tsms  39074  sge0f1o  39076  sge0pr  39088  sge0resplit  39100  sge0split  39103  sge0iunmptlemre  39109  sge0isummpt2  39126  carageniuncllem1  39212  hoicvr  39239  hoicvrrex  39247  hoidmvlelem2  39287  hspmbl  39320  smfmullem4  39480  prmdvdsfmtnof1lem1  39836  prmdvdsfmtnof  39838  upgrss  40313  pthdivtx  40934  av-disjxwwlkn  41118  oddibas  41602  2zrngbas  41725  2zrng0  41727  aacllem  42316  amgmlemALT  42318
  Copyright terms: Public domain W3C validator