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

Theorem sstri 3753
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 3751 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  snsstp1  4492  snsstp2  4493  uniintsn  4666  ssrnres  5730  cossxp  5819  foimacnv  6315  ssimaex  6425  riotassuni  6811  oprabss  6911  dmexg  7262  rnexg  7263  fabexg  7287  fparlem3  7447  fparlem4  7448  snopsuppss  7478  tposssxp  7525  mapsspw  8059  sbthlem5  8239  sbthlem7  8241  cnvimamptfin  8432  marypha1lem  8504  ordtypelem4  8591  hartogslem1  8612  tc2  8791  tz9.12lem1  8823  rankval4  8903  rankxpl  8911  rankmapu  8914  rankxplim  8915  djuin  8948  infxpenlem  9026  ackbij1lem18  9251  cflm  9264  fin23lem29  9355  hsmexlem4  9443  hsmexlem5  9444  brdom3  9542  brdom5  9543  brdom4  9544  smobeth  9600  pwfseqlem3  9674  wundm  9742  wunrn  9743  wunex2  9752  ltsopi  9902  dmaddpi  9904  dmmulpi  9905  nqerf  9944  ltrelxr  10291  nnsscn  11217  nn0sscn  11489  uzwo2  11945  infssuzle  11964  infssuzcl  11965  uzwo3  11976  nn0ssq  11989  nnssq  11990  qsscn  11992  rpnnen1lem3  12009  rpnnen1lem5  12011  rpnnen1lem3OLD  12015  rpnnen1lem5OLD  12017  dflt2  12174  fzval2  12522  fzof  12661  fzossnn  12711  injresinj  12783  flval3  12810  uzsup  12856  uzrdgfni  12951  expcl2lem  13066  rpexpcl  13073  expge0  13090  expge1  13091  hashxrcl  13340  seqcoll  13440  wrdexg  13501  xptrrel  13920  trclublem  13935  sqrlem3  14184  limsupval2  14410  limsupgre  14411  rlimpm  14430  rlimclim  14476  isercolllem1  14594  isercolllem2  14595  isercoll  14597  caurcvg  14606  caucvg  14608  summolem2a  14645  summolem2  14646  zsum  14648  fsumcvg3  14659  fsumrpcl  14667  fsumge0  14726  climfsum  14751  ackbijnn  14759  prodmolem2a  14863  prodmolem2  14864  zprod  14866  fprodrpcl  14885  fprodge0  14923  fprodge1  14925  rprisefaccl  14953  divalglem8  15325  sadaddlem  15390  lcmfval  15536  isprm3  15598  maxprmfct  15623  pclem  15745  prmreclem1  15822  prmreclem2  15823  prmreclem3  15824  1arith  15833  4sqlem11  15861  ramtlecl  15906  ramcl2lem  15915  ramxrcl  15923  prmgaplem3  15959  prmgaplem4  15960  cshwshashlem1  16004  structfn  16076  strlemor1OLD  16171  strleun  16174  srngbase  16211  srngplusg  16212  srngmulr  16213  lmodbase  16220  lmodplusg  16221  lmodsca  16222  ipsbase  16227  ipsaddg  16228  ipsmulr  16229  ipssca  16230  ipsvsca  16231  ipsip  16232  phlbase  16237  phlplusg  16238  phlsca  16239  phlvsca  16240  phlip  16241  odrngbas  16269  odrngplusg  16270  odrngmulr  16271  odrngtset  16272  odrngle  16273  odrngds  16274  prdsval  16317  prdssca  16318  prdsbas  16319  prdsplusg  16320  prdsmulr  16321  prdsvsca  16322  prdsip  16323  prdsle  16324  prdsds  16326  prdstset  16328  prdshom  16329  prdsco  16330  imasbas  16374  imasds  16375  imasplusg  16379  imasmulr  16380  imassca  16381  imasvsca  16382  imasip  16383  imastset  16384  imasle  16385  wunfunc  16760  fullfunc  16767  fthfunc  16768  isfull  16771  isfth  16775  wunnat  16817  dmcoass  16917  catcisolem  16957  catciso  16958  catcoppccl  16959  catcfuccl  16960  catcxpccl  17048  ipobas  17356  ipolerval  17357  ipotset  17358  psdmrn  17408  psss  17415  ledm  17425  lern  17426  dirdm  17435  dirge  17438  mvdco  18065  f1omvdconj  18066  gexex  18456  gsumval3  18508  lssacs  19169  asplss  19531  aspsubrg  19533  psrass1lem  19579  psrbas  19580  psrplusg  19583  psrmulr  19586  psrsca  19591  psrvscafval  19592  psrass1  19607  psrass23l  19610  psrcom  19611  psrass23  19612  psropprmul  19810  coe1mul2  19841  cnfldbas  19952  cnfldadd  19953  cnfldmul  19954  cnfldcj  19955  cnfldtset  19956  cnfldle  19957  cnfldds  19958  cnfldunif  19959  rge0srg  20019  zntoslem  20107  ofco2  20459  toponsspwpw  20928  dmtopon  20929  leordtval2  21218  lmbrf  21266  lmres  21306  fiuncmp  21409  comppfsc  21537  1stckgenlem  21558  kgencn3  21563  ptbasfi  21586  xkoopn  21594  txcnmpt  21629  txkgen  21657  opnfbas  21847  fmfnfmlem4  21962  tsmsxplem1  22157  trust  22234  restutop  22242  nmoffn  22716  nmofval  22719  nmogelb  22721  nmolb  22722  nmof  22724  qtopbas  22764  tgqioo  22804  re2ndc  22805  iitopon  22883  dfii3  22887  iimulcn  22938  cnheiborlem  22954  bndth  22958  lebnumii  22966  reparphti  22997  pcoass  23024  cphsqrtcl  23184  lmmbrf  23260  iscauf  23278  caucfil  23281  lmclimf  23302  rrxmval  23388  rrxmet  23391  ovolfioo  23436  ovolficc  23437  ovolficcss  23438  ovolfsf  23440  ovollb  23447  ovolicc2lem3  23487  ovolicc2lem4  23488  ovolicc2  23490  volf  23497  volsup  23524  ovolfs2  23539  uniiccdif  23546  uniioovol  23547  uniiccvol  23548  uniioombllem2  23551  uniioombllem3a  23552  uniioombllem3  23553  uniioombllem4  23554  uniioombllem5  23555  uniioombl  23557  dyadmbllem  23567  dyadmbl  23568  opnmbllem  23569  opnmblALT  23571  volsup2  23573  vitalilem4  23579  vitalilem5  23580  vitali  23581  mbfimaopnlem  23621  mbflimsup  23632  i1f0  23653  i1f1  23656  itg11  23657  itg2mulc  23713  itg2gt0  23726  ellimc2  23840  limcresi  23848  dvreslem  23872  dvres2lem  23873  dvaddbr  23900  dvmulbr  23901  dvlipcn  23956  c1liplem1  23958  lhop1lem  23975  lhop1  23976  lhop2  23977  lhop  23978  dvfsumrlim  23993  ftc1cn  24005  itgsubstlem  24010  itgsubst  24011  mdegleb  24023  mdeglt  24024  mdegldg  24025  mdegxrcl  24026  mdegcl  24028  mdegaddle  24033  mdegmullem  24037  deg1mul3le  24075  ig1peu  24130  ig1pdvds  24135  aacjcl  24281  aannenlem2  24283  aannenlem3  24284  aalioulem2  24287  taylfval  24312  radcnvcl  24370  radcnvlt1  24371  radcnvle  24373  abelth  24394  abelth2  24395  pilem2  24405  pilem3  24406  pige3  24468  recosf1o  24480  resinf1o  24481  tanord1  24482  logcn  24592  dvlog  24596  dvlog2lem  24597  efopn  24603  logtayl  24605  cxpcn3  24688  loglesqrt  24698  ssscongptld  24751  leibpi  24868  efrlim  24895  jensenlem1  24912  jensenlem2  24913  jensen  24914  amgm  24916  lgamgulmlem2  24955  ftalem5  25002  efnnfsumcl  25028  efchtdvds  25084  dvdsmulf1o  25119  fsumdvdsmul  25120  lgsfcl2  25227  2sqlem6  25347  2sqlem8  25350  2sqlem9  25351  rpvmasumlem  25375  rpvmasum2  25400  dchrisum0re  25401  dchrisum0lem3  25407  dchrisum0  25408  rplogsum  25415  dirith2  25416  axtgcgrrflx  25560  axtgcgrid  25561  axtgsegcon  25562  axtg5seg  25563  axtgbtwnid  25564  axtgpasch  25565  axtgcont1  25566  tgcgr4  25625  motcgrg  25638  tglng  25640  upgrss  26182  pthdivtx  26835  disjxwwlkn  27031  nmlno0lem  27957  hlimcaui  28402  chsspwh  28413  shsss  28481  chintcli  28499  shsleji  28538  shub1i  28542  shsval2i  28555  lejdii  28706  spanuni  28712  sshhococi  28714  spansnpji  28746  osumcori  28811  5oai  28829  3oalem6  28835  3oai  28836  pjssmii  28849  mayete3i  28896  mayetes3i  28897  nmlnop0iALT  29163  imaelshi  29226  pjnmopi  29316  pjclem1  29363  pjci  29368  mdslmd1lem1  29493  shatomistici  29529  hatomistici  29530  chpssati  29531  xppreima  29758  iundisjfi  29864  iundisj2fi  29865  fprodex01  29880  xrsmulgzz  29987  fsumrp0cl  30004  gsummpt2co  30089  xrge0slmod  30153  unitsscn  30251  ordtconnlem1  30279  xrge0iifhom  30292  lmlimxrge0  30303  lmxrge0  30307  indsumin  30393  esumcst  30434  esumpfinvallem  30445  esumpfinval  30446  esumpfinvalf  30447  esumcvg  30457  imambfm  30633  elmbfmvol2  30638  sxbrsigalem3  30643  sxbrsigalem2  30657  sxbrsigalem4  30658  sitgclg  30713  eulerpartlem1  30738  eulerpartlemgvv  30747  eulerpartlemgh  30749  eulerpartlemgf  30750  ballotlemfc0  30863  ballotlemfcc  30864  ballotlemiex  30872  ballotlemsup  30875  ballotlemsdom  30882  ballotlemsima  30886  ballotlemrv2  30892  ballotth  30908  signsplypnf  30936  signsply0  30937  rpsqrtcn  30980  itgexpif  30993  fsum2dsub  30994  reprfi2  31010  chtvalz  31016  breprexplemc  31019  breprexpnat  31021  circlemeth  31027  circlemethnat  31028  circlevma  31029  circlemethhgt  31030  hgt750lemd  31035  hgt750lema  31044  tgoldbachgtde  31047  tgoldbachgtda  31048  tgoldbachgt  31050  bnj1145  31368  bnj1286  31394  subfacp1lem2a  31469  erdszelem4  31483  erdszelem5  31484  erdszelem7  31486  erdszelem8  31487  kur14lem7  31501  kur14lem9  31503  cvxpconn  31531  cvxsconn  31532  resconn  31535  iccllysconn  31539  noextendseq  32126  txpss3v  32291  txprel  32292  limitssson  32324  finminlem  32618  tailf  32676  filnetlem3  32681  onint1  32754  bj-unrab  33228  bj-2upln1upl  33318  bj-rrvecsscmn  33463  taupilem2  33479  taupi  33480  poimirlem3  33725  poimirlem30  33752  poimirlem31  33753  poimirlem32  33754  broucube  33756  opnmbllem0  33758  mblfinlem1  33759  mblfinlem2  33760  mblfinlem3  33761  mblfinlem4  33762  ismblfin  33763  mbfposadd  33770  cnambfre  33771  itg2addnc  33777  ftc1cnnclem  33796  ftc1cnnc  33797  ftc1anclem3  33800  ftc1anclem7  33804  ftc1anc  33806  ftc2nc  33807  dvreasin  33811  dvreacos  33812  areacirclem1  33813  areacirclem2  33814  areacirc  33818  caures  33869  reheibor  33951  xrnss3v  34457  xrnrel  34458  atlatmstc  35109  atlatle  35110  pmaple  35550  sspadd1  35604  sspadd2  35605  diophin  37838  4rexfrabdioph  37864  6rexfrabdioph  37865  irrapxlem1  37888  irrapx1  37894  monotuz  38008  jm2.27dlem5  38082  hbtlem2  38196  algbase  38250  algaddg  38251  algmulr  38252  algsca  38253  algvsca  38254  itgpowd  38302  arearect  38303  areaquad  38304  rtrclex  38426  trclubgNEW  38427  trclexi  38429  rtrclexi  38430  cnvtrcl0  38435  dfrtrcl5  38438  trrelsuperrel2dg  38465  relexpaddss  38512  brtrclfv2  38521  frege131d  38558  xphe  38577  idhe  38583  clsk3nimkb  38840  gneispace  38934  k0004val0  38954  lhe4.4ex1a  39030  uzmptshftfval  39047  binomcxplemdvbinom  39054  binomcxplemcvg  39055  binomcxplemnotnn0  39057  relopabVD  39636  fzisoeu  40013  fzsscn  40024  fzssre  40027  fzossuz  40096  fzossz  40097  uzssre  40118  zssxr  40119  uzssre2  40131  supminfxr  40192  uzsscn  40204  rpssxr  40209  ioosscn  40219  uzinico  40290  limcresiooub  40377  limcresioolb  40378  limcleqr  40379  limclner  40386  limclr  40390  limsupequzmpt2  40453  liminfval2  40503  liminfequzmpt2  40526  icccncfext  40603  cncficcgt0  40604  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnprodlem1  40664  dvnprodlem2  40665  itgsin0pilem1  40668  itgsinexplem1  40672  itgsinexp  40673  dirkercncflem2  40824  fourierdlem16  40843  fourierdlem18  40845  fourierdlem20  40847  fourierdlem21  40848  fourierdlem22  40849  fourierdlem25  40852  fourierdlem37  40864  fourierdlem42  40869  fourierdlem50  40876  fourierdlem52  40878  fourierdlem62  40888  fourierdlem64  40890  fourierdlem66  40892  fourierdlem68  40894  fourierdlem74  40900  fourierdlem75  40901  fourierdlem76  40902  fourierdlem79  40905  fourierdlem83  40909  fourierdlem95  40921  fourierdlem101  40927  fourierdlem102  40928  fourierdlem103  40929  fourierdlem104  40930  fourierdlem112  40938  fourierdlem114  40940  sqwvfoura  40948  sqwvfourb  40949  fouriersw  40951  etransclem24  40978  etransclem48  41002  sge0sn  41099  sge0tsms  41100  sge0f1o  41102  sge0pr  41114  sge0resplit  41126  sge0split  41129  sge0iunmptlemre  41135  sge0isummpt2  41152  carageniuncllem1  41241  hoicvr  41268  hoicvrrex  41276  hoidmvlelem2  41316  hspmbl  41349  smfmullem4  41507  prmdvdsfmtnof1lem1  42006  prmdvdsfmtnof  42008  oddibas  42323  2zrngbas  42446  2zrng0  42448  aacllem  43060  amgmlemALT  43062
  Copyright terms: Public domain W3C validator