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

Theorem sstri 3577
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 3575 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  snsstp1  4287  snsstp2  4288  uniintsn  4449  ssrnres  5491  cossxp  5575  foimacnv  6067  ssimaex  6173  riotassuni  6547  oprabss  6644  dmexg  6989  rnexg  6990  fabexg  7015  fparlem3  7166  fparlem4  7167  snopsuppss  7197  tposssxp  7243  mapsspw  7779  sbthlem5  7959  sbthlem7  7961  cnvimamptfin  8150  marypha1lem  8222  ordtypelem4  8309  hartogslem1  8330  tc2  8501  tz9.12lem1  8533  rankval4  8613  rankxpl  8621  rankmapu  8624  rankxplim  8625  infxpenlem  8719  ackbij1lem18  8942  cflm  8955  fin23lem29  9046  hsmexlem4  9134  hsmexlem5  9135  brdom3  9231  brdom5  9232  brdom4  9233  smobeth  9287  pwfseqlem3  9361  wundm  9429  wunrn  9430  wunex2  9439  ltsopi  9589  dmaddpi  9591  dmmulpi  9592  nqerf  9631  ltrelxr  9978  nnsscn  10902  nn0sscn  11174  uzwo2  11628  infssuzle  11647  infssuzcl  11648  uzwo3  11659  nn0ssq  11672  nnssq  11673  qsscn  11675  rpnnen1lem3  11692  rpnnen1lem5  11694  rpnnen1lem3OLD  11698  rpnnen1lem5OLD  11700  dflt2  11857  fzval2  12200  fzof  12336  fzossnn  12384  fzo0ssnn0OLD  12416  injresinj  12451  flval3  12478  uzsup  12524  uzrdgfni  12619  expcl2lem  12734  rpexpcl  12741  expge0  12758  expge1  12759  hashxrcl  13010  seqcoll  13105  wrdexg  13170  xptrrel  13567  trclublem  13582  sqrlem3  13833  limsupval2  14059  limsupgre  14060  rlimpm  14079  rlimclim  14125  isercolllem1  14243  isercolllem2  14244  isercoll  14246  caurcvg  14255  caucvg  14257  summolem2a  14293  summolem2  14294  zsum  14296  fsumcvg3  14307  fsumrpcl  14315  fsumge0  14368  climfsum  14393  ackbijnn  14399  prodmolem2a  14503  prodmolem2  14504  zprod  14506  fprodrpcl  14525  fprodge0  14563  fprodge1  14565  rprisefaccl  14593  divalglem8  14961  sadaddlem  15026  lcmfval  15172  isprm3  15234  maxprmfct  15259  pclem  15381  prmreclem1  15458  prmreclem2  15459  prmreclem3  15460  1arith  15469  4sqlem11  15497  ramtlecl  15542  ramcl2lem  15551  ramxrcl  15559  prmgaplem3  15595  prmgaplem4  15596  cshwshashlem1  15640  structfn  15708  strlemor1  15796  strleun  15799  srngbase  15832  srngplusg  15833  srngmulr  15834  lmodbase  15841  lmodplusg  15842  lmodsca  15843  ipsbase  15848  ipsaddg  15849  ipsmulr  15850  ipssca  15851  ipsvsca  15852  ipsip  15853  phlbase  15858  phlplusg  15859  phlsca  15860  phlvsca  15861  phlip  15862  odrngbas  15890  odrngplusg  15891  odrngmulr  15892  odrngtset  15893  odrngle  15894  odrngds  15895  prdsval  15938  prdssca  15939  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdsip  15944  prdsle  15945  prdsds  15947  prdstset  15949  prdshom  15950  prdsco  15951  imasbas  15995  imasds  15996  imasplusg  16000  imasmulr  16001  imassca  16002  imasvsca  16003  imasip  16004  imastset  16005  imasle  16006  wunfunc  16382  fullfunc  16389  fthfunc  16390  isfull  16393  isfth  16397  wunnat  16439  dmcoass  16539  catcisolem  16579  catciso  16580  catcoppccl  16581  catcfuccl  16582  catcxpccl  16670  ipobas  16978  ipolerval  16979  ipotset  16980  psdmrn  17030  psss  17037  ledm  17047  lern  17048  dirdm  17057  dirge  17060  mvdco  17688  f1omvdconj  17689  gexex  18079  gsumval3  18131  lssacs  18788  asplss  19150  aspsubrg  19152  psrass1lem  19198  psrbas  19199  psrplusg  19202  psrmulr  19205  psrsca  19210  psrvscafval  19211  psrass1  19226  psrass23l  19229  psrcom  19230  psrass23  19231  psropprmul  19429  coe1mul2  19460  cnfldbas  19571  cnfldadd  19572  cnfldmul  19573  cnfldcj  19574  cnfldtset  19575  cnfldle  19576  cnfldds  19577  cnfldunif  19578  rge0srg  19636  zntoslem  19724  ofco2  20076  leordtval2  20826  lmbrf  20874  lmres  20914  fiuncmp  21017  comppfsc  21145  1stckgenlem  21166  kgencn3  21171  ptbasfi  21194  xkoopn  21202  txcnmpt  21237  txkgen  21265  opnfbas  21456  fmfnfmlem4  21571  tsmsxplem1  21766  trust  21843  restutop  21851  nmoffn  22325  nmofval  22328  nmogelb  22330  nmolb  22331  nmof  22333  qtopbas  22373  tgqioo  22411  re2ndc  22412  iitopon  22490  dfii3  22494  iimulcn  22545  cnheiborlem  22561  bndth  22565  lebnumii  22573  reparphti  22605  pcoass  22632  cphsqrtcl  22792  lmmbrf  22868  iscauf  22886  caucfil  22889  lmclimf  22910  rrxmval  22996  rrxmet  22999  ovolfioo  23043  ovolficc  23044  ovolficcss  23045  ovolfsf  23047  ovollb  23054  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2  23097  volf  23104  volsup  23131  ovolfs2  23145  uniiccdif  23152  uniioovol  23153  uniiccvol  23154  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem5  23161  uniioombl  23163  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  opnmblALT  23177  volsup2  23179  vitalilem4  23186  vitalilem5  23187  vitali  23188  mbfimaopnlem  23228  mbflimsup  23239  i1f0  23260  i1f1  23263  itg11  23264  itg2mulc  23320  itg2gt0  23333  ellimc2  23447  limcresi  23455  dvreslem  23479  dvres2lem  23480  dvaddbr  23507  dvmulbr  23508  dvlipcn  23561  c1liplem1  23563  lhop1lem  23580  lhop1  23581  lhop2  23582  lhop  23583  dvfsumrlim  23598  ftc1cn  23610  itgsubstlem  23615  itgsubst  23616  mdegleb  23628  mdeglt  23629  mdegldg  23630  mdegxrcl  23631  mdegcl  23633  mdegaddle  23638  mdegmullem  23642  deg1mul3le  23680  ig1peu  23735  ig1pdvds  23740  aacjcl  23886  aannenlem2  23888  aannenlem3  23889  aalioulem2  23892  taylfval  23917  radcnvcl  23975  radcnvlt1  23976  radcnvle  23978  abelth  23999  abelth2  24000  pilem2  24010  pilem3  24011  pige3  24073  recosf1o  24085  resinf1o  24086  tanord1  24087  logcn  24193  dvlog  24197  dvlog2lem  24198  efopn  24204  logtayl  24206  cxpcn3  24289  loglesqrt  24299  ssscongptld  24352  leibpi  24469  efrlim  24496  jensenlem1  24513  jensenlem2  24514  jensen  24515  amgm  24517  lgamgulmlem2  24556  ftalem5  24603  efnnfsumcl  24629  efchtdvds  24685  dvdsmulf1o  24720  fsumdvdsmul  24721  lgsfcl2  24828  2sqlem6  24948  2sqlem8  24951  2sqlem9  24952  rpvmasumlem  24976  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem3  25008  dchrisum0  25009  rplogsum  25016  dirith2  25017  axtgcgrrflx  25161  axtgcgrid  25162  axtgsegcon  25163  axtg5seg  25164  axtgbtwnid  25165  axtgpasch  25166  axtgcont1  25167  tgcgr4  25226  motcgrg  25239  tglng  25241  upgrss  25755  umgrass  25848  constr3pthlem1  26183  disjxwwlkn  26273  nmlno0lem  27032  hlimcaui  27477  chsspwh  27488  shsss  27556  chintcli  27574  shsleji  27613  shub1i  27617  shsval2i  27630  lejdii  27781  spanuni  27787  sshhococi  27789  spansnpji  27821  osumcori  27886  5oai  27904  3oalem6  27910  3oai  27911  pjssmii  27924  mayete3i  27971  mayetes3i  27972  nmlnop0iALT  28238  imaelshi  28301  pjnmopi  28391  pjclem1  28438  pjci  28443  mdslmd1lem1  28568  shatomistici  28604  hatomistici  28605  chpssati  28606  xppreima  28829  iundisjfi  28942  iundisj2fi  28943  xrsmulgzz  29009  fsumrp0cl  29026  gsummpt2co  29111  xrge0slmod  29175  unitsscn  29270  ordtconlem1  29298  xrge0iifhom  29311  lmlimxrge0  29322  lmxrge0  29326  esumcst  29452  esumpfinvallem  29463  esumpfinval  29464  esumpfinvalf  29465  esumcvg  29475  imambfm  29651  elmbfmvol2  29656  sxbrsigalem3  29661  sxbrsigalem2  29675  sxbrsigalem4  29676  sitgclg  29731  eulerpartlem1  29756  eulerpartlemgvv  29765  eulerpartlemgh  29767  eulerpartlemgf  29768  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemiex  29890  ballotlemsup  29893  ballotlemsdom  29900  ballotlemsima  29904  ballotlemrv2  29910  ballotth  29926  signsplypnf  29953  signsply0  29954  bnj1145  30315  bnj1286  30341  subfacp1lem2a  30416  erdszelem4  30430  erdszelem5  30431  erdszelem7  30433  erdszelem8  30434  kur14lem7  30448  kur14lem9  30450  cvxpcon  30478  cvxscon  30479  rescon  30482  iccllyscon  30486  txpss3v  31155  txprel  31156  limitssson  31188  finminlem  31482  tailf  31540  filnetlem3  31545  onint1  31618  bj-unrab  32114  bj-2upln1upl  32205  bj-toponss  32241  bj-dmtopon  32242  bj-rrvecsscmn  32329  taupilem2  32345  taupi  32346  poimirlem3  32582  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  broucube  32613  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  mbfposadd  32627  cnambfre  32628  itg2addnc  32634  ftc1cnnclem  32653  ftc1cnnc  32654  ftc1anclem3  32657  ftc1anclem7  32661  ftc1anc  32663  ftc2nc  32664  dvreasin  32668  dvreacos  32669  areacirclem1  32670  areacirclem2  32671  areacirc  32675  caures  32726  reheibor  32808  atlatmstc  33624  atlatle  33625  pmaple  34065  sspadd1  34119  sspadd2  34120  diophin  36354  4rexfrabdioph  36380  6rexfrabdioph  36381  irrapxlem1  36404  irrapx1  36410  monotuz  36524  jm2.27dlem5  36598  hbtlem2  36713  algbase  36767  algaddg  36768  algmulr  36769  algsca  36770  algvsca  36771  itgpowd  36819  arearect  36820  areaquad  36821  rtrclex  36943  trclubgNEW  36944  trclexi  36946  rtrclexi  36947  cnvtrcl0  36952  dfrtrcl5  36955  trrelsuperrel2dg  36982  relexpaddss  37029  brtrclfv2  37038  frege131d  37075  xphe  37095  idhe  37101  clsk3nimkb  37358  gneispace  37452  k0004val0  37472  lhe4.4ex1a  37550  uzmptshftfval  37567  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemnotnn0  37577  relopabVD  38159  fzisoeu  38455  fzsscn  38467  fzssre  38470  fzossuz  38539  fzossz  38540  ioosscn  38563  limcresiooub  38709  limcresioolb  38710  limcleqr  38711  limclner  38718  limclr  38722  icccncfext  38773  cncficcgt0  38774  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem1  38836  dvnprodlem2  38837  itgsin0pilem1  38841  itgsinexplem1  38845  itgsinexp  38846  dirkercncflem2  38997  fourierdlem16  39016  fourierdlem18  39018  fourierdlem20  39020  fourierdlem21  39021  fourierdlem22  39022  fourierdlem25  39025  fourierdlem37  39037  fourierdlem42  39042  fourierdlem50  39049  fourierdlem52  39051  fourierdlem62  39061  fourierdlem64  39063  fourierdlem66  39065  fourierdlem68  39067  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem79  39078  fourierdlem83  39082  fourierdlem95  39094  fourierdlem101  39100  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem24  39151  etransclem48  39175  sge0sn  39272  sge0tsms  39273  sge0f1o  39275  sge0pr  39287  sge0resplit  39299  sge0split  39302  sge0iunmptlemre  39308  sge0isummpt2  39325  carageniuncllem1  39411  hoicvr  39438  hoicvrrex  39446  hoidmvlelem2  39486  hspmbl  39519  smfmullem4  39679  prmdvdsfmtnof1lem1  40034  prmdvdsfmtnof  40036  pthdivtx  40935  av-disjxwwlkn  41119  oddibas  41603  2zrngbas  41726  2zrng0  41728  aacllem  42356  amgmlemALT  42358
  Copyright terms: Public domain W3C validator