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

Theorem sstri 3818
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 3816 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-in 3787  df-ss 3794
This theorem is referenced by:  snsstp1  4548  snsstp2  4549  uniintsn  4717  ssrnres  5797  cossxp  5886  foimacnv  6380  ssimaex  6494  riotassuni  6882  oprabss  6986  dmexg  7337  rnexg  7338  fabexg  7362  fparlem3  7523  fparlem4  7524  snopsuppss  7554  tposssxp  7601  mapsspw  8138  sbthlem5  8323  sbthlem7  8325  cnvimamptfin  8516  marypha1lem  8588  ordtypelem4  8675  hartogslem1  8696  tc2  8875  tz9.12lem1  8907  rankval4  8987  rankxpl  8995  rankmapu  8998  rankxplim  8999  djuin  9037  infxpenlem  9129  ackbij1lem18  9354  cflm  9367  fin23lem29  9458  hsmexlem4  9546  hsmexlem5  9547  brdom3  9645  brdom5  9646  brdom4  9647  smobeth  9703  pwfseqlem3  9777  wundm  9845  wunrn  9846  wunex2  9855  ltsopi  10005  dmaddpi  10007  dmmulpi  10008  nqerf  10047  ltrelxr  10394  nnsscnOLD  11321  nn0sscn  11584  uzwo2  11991  infssuzle  12010  infssuzcl  12011  uzwo3  12022  nn0ssq  12035  nnssq  12036  qsscn  12038  rpnnen1lem3  12055  rpnnen1lem5  12057  dflt2  12217  fzval2  12572  fzof  12711  fzossnn  12761  injresinj  12833  flval3  12860  uzsup  12906  uzrdgfni  13001  expcl2lem  13115  rpexpcl  13122  expge0  13139  expge1  13140  hashxrcl  13386  seqcoll  13485  wrdexg  13546  xptrrel  13964  trclublem  13979  sqrlem3  14228  limsupval2  14454  limsupgre  14455  rlimpm  14474  rlimclim  14520  isercolllem1  14638  isercolllem2  14639  isercoll  14641  caurcvg  14650  caucvg  14652  summolem2a  14689  summolem2  14690  zsum  14692  fsumcvg3  14703  fsumrpcl  14711  fsumge0  14769  climfsum  14794  ackbijnn  14802  prodmolem2a  14905  prodmolem2  14906  zprod  14908  fprodrpcl  14927  fprodge0  14964  fprodge1  14966  rprisefaccl  14994  divalglem8  15363  sadaddlem  15427  lcmfval  15573  isprm3  15634  maxprmfct  15658  pclem  15780  prmreclem1  15857  prmreclem2  15858  prmreclem3  15859  1arith  15868  4sqlem11  15896  ramtlecl  15941  ramcl2lem  15950  ramxrcl  15958  prmgaplem3  15994  prmgaplem4  15995  cshwshashlem1  16034  structfn  16105  strlemor1OLD  16200  strleun  16203  srngbase  16240  srngplusg  16241  srngmulr  16242  lmodbase  16249  lmodplusg  16250  lmodsca  16251  ipsbase  16256  ipsaddg  16257  ipsmulr  16258  ipssca  16259  ipsvsca  16260  ipsip  16261  phlbase  16266  phlplusg  16267  phlsca  16268  phlvsca  16269  phlip  16270  odrngbas  16292  odrngplusg  16293  odrngmulr  16294  odrngtset  16295  odrngle  16296  odrngds  16297  prdsval  16340  prdssca  16341  prdsbas  16342  prdsplusg  16343  prdsmulr  16344  prdsvsca  16345  prdsip  16346  prdsle  16347  prdsds  16349  prdstset  16351  prdshom  16352  prdsco  16353  imasbas  16397  imasds  16398  imasplusg  16402  imasmulr  16403  imassca  16404  imasvsca  16405  imasip  16406  imastset  16407  imasle  16408  wunfunc  16783  fullfunc  16790  fthfunc  16791  isfull  16794  isfth  16798  wunnat  16840  dmcoass  16940  catcisolem  16980  catciso  16981  catcoppccl  16982  catcfuccl  16983  catcxpccl  17072  ipobas  17380  ipolerval  17381  ipotset  17382  psdmrn  17432  psss  17439  ledm  17449  lern  17450  dirdm  17459  dirge  17462  mvdco  18086  f1omvdconj  18087  gexex  18477  gsumval3  18529  lssacs  19194  asplss  19558  aspsubrg  19560  psrass1lem  19606  psrbas  19607  psrplusg  19610  psrmulr  19613  psrsca  19618  psrvscafval  19619  psrass1  19634  psrass23l  19637  psrcom  19638  psrass23  19639  psropprmul  19836  coe1mul2  19867  cnfldbas  19978  cnfldadd  19979  cnfldmul  19980  cnfldcj  19981  cnfldtset  19982  cnfldle  19983  cnfldds  19984  cnfldunif  19985  rge0srg  20045  zntoslem  20132  ofco2  20489  toponsspwpw  20961  dmtopon  20962  leordtval2  21251  lmbrf  21299  lmres  21339  fiuncmp  21442  comppfsc  21570  1stckgenlem  21591  kgencn3  21596  ptbasfi  21619  xkoopn  21627  txcnmpt  21662  txkgen  21690  opnfbas  21880  fmfnfmlem4  21995  tsmsxplem1  22190  trust  22267  restutop  22275  nmoffn  22749  nmofval  22752  nmogelb  22754  nmolb  22755  nmof  22757  qtopbas  22797  tgqioo  22837  re2ndc  22838  iitopon  22916  dfii3  22920  iimulcn  22971  cnheiborlem  22987  bndth  22991  lebnumii  22999  reparphti  23030  pcoass  23057  cphsqrtcl  23217  lmmbrf  23294  iscauf  23312  caucfil  23315  lmclimf  23336  rrxmval  23423  rrxmet  23426  ovolfioo  23471  ovolficc  23472  ovolficcss  23473  ovolfsf  23475  ovollb  23483  ovolicc2lem3  23523  ovolicc2lem4  23524  ovolicc2  23526  volf  23533  volsup  23560  ovolfs2  23575  uniiccdif  23582  uniioovol  23583  uniiccvol  23584  uniioombllem2  23587  uniioombllem3a  23588  uniioombllem3  23589  uniioombllem4  23590  uniioombllem5  23591  uniioombl  23593  dyadmbllem  23603  dyadmbl  23604  opnmbllem  23605  opnmblALT  23607  volsup2  23609  vitalilem4  23615  vitalilem5  23616  vitali  23617  mbfimaopnlem  23659  mbflimsup  23670  i1f0  23691  i1f1  23694  itg11  23695  itg2mulc  23751  itg2gt0  23764  ellimc2  23878  limcresi  23886  dvreslem  23910  dvres2lem  23911  dvaddbr  23938  dvmulbr  23939  dvlipcn  23994  c1liplem1  23996  lhop1lem  24013  lhop1  24014  lhop2  24015  lhop  24016  dvfsumrlim  24031  ftc1cn  24043  itgsubstlem  24048  itgsubst  24049  mdegleb  24061  mdeglt  24062  mdegldg  24063  mdegxrcl  24064  mdegcl  24066  mdegaddle  24071  mdegmullem  24075  deg1mul3le  24113  ig1peu  24168  ig1pdvds  24173  aacjcl  24319  aannenlem2  24321  aannenlem3  24322  aalioulem2  24325  taylfval  24350  radcnvcl  24408  radcnvlt1  24409  radcnvle  24411  abelth  24432  abelth2  24433  pilem2  24443  pilem3  24444  pilem3OLD  24445  pige3  24507  recosf1o  24519  resinf1o  24520  tanord1  24521  logcn  24630  dvlog  24634  dvlog2lem  24635  efopn  24641  logtayl  24643  cxpcn3  24726  loglesqrt  24736  ssscongptld  24789  leibpi  24906  efrlim  24933  jensenlem1  24950  jensenlem2  24951  jensen  24952  amgm  24954  lgamgulmlem2  24993  ftalem5  25040  efnnfsumcl  25066  efchtdvds  25122  dvdsmulf1o  25157  fsumdvdsmul  25158  lgsfcl2  25265  2sqlem6  25385  2sqlem8  25388  2sqlem9  25389  rpvmasumlem  25413  rpvmasum2  25438  dchrisum0re  25439  dchrisum0lem3  25445  dchrisum0  25446  rplogsum  25453  dirith2  25454  axtgcgrrflx  25598  axtgcgrid  25599  axtgsegcon  25600  axtg5seg  25601  axtgbtwnid  25602  axtgpasch  25603  axtgcont1  25604  tgcgr4  25663  motcgrg  25676  tglng  25678  upgrss  26220  pthdivtx  26876  disjxwwlkn  27074  nmlno0lem  27999  hlimcaui  28444  chsspwh  28455  shsss  28523  chintcli  28541  shsleji  28580  shub1i  28584  shsval2i  28597  lejdii  28748  spanuni  28754  sshhococi  28756  spansnpji  28788  osumcori  28853  5oai  28871  3oalem6  28877  3oai  28878  pjssmii  28891  mayete3i  28938  mayetes3i  28939  nmlnop0iALT  29205  imaelshi  29268  pjnmopi  29358  pjclem1  29405  pjci  29410  mdslmd1lem1  29535  shatomistici  29571  hatomistici  29572  chpssati  29573  xppreima  29799  iundisjfi  29905  iundisj2fi  29906  fprodex01  29921  xrsmulgzz  30026  fsumrp0cl  30043  gsummpt2co  30128  xrge0slmod  30192  unitsscn  30290  ordtconnlem1  30318  xrge0iifhom  30331  lmlimxrge0  30342  lmxrge0  30346  indsumin  30432  esumcst  30473  esumpfinvallem  30484  esumpfinval  30485  esumpfinvalf  30486  esumcvg  30496  imambfm  30672  elmbfmvol2  30677  sxbrsigalem3  30682  sxbrsigalem2  30696  sxbrsigalem4  30697  sitgclg  30752  eulerpartlem1  30777  eulerpartlemgvv  30786  eulerpartlemgh  30788  eulerpartlemgf  30789  ballotlemfc0  30902  ballotlemfcc  30903  ballotlemiex  30911  ballotlemsup  30914  ballotlemsdom  30921  ballotlemsima  30925  ballotlemrv2  30931  ballotth  30947  signsplypnf  30975  signsply0  30976  rpsqrtcn  31019  itgexpif  31032  fsum2dsub  31033  reprfi2  31049  chtvalz  31055  breprexplemc  31058  breprexpnat  31060  circlemeth  31066  circlemethnat  31067  circlevma  31068  circlemethhgt  31069  hgt750lemd  31074  hgt750lema  31083  tgoldbachgtde  31086  tgoldbachgtda  31087  tgoldbachgt  31089  bnj1145  31406  bnj1286  31432  subfacp1lem2a  31507  erdszelem4  31521  erdszelem5  31522  erdszelem7  31524  erdszelem8  31525  kur14lem7  31539  kur14lem9  31541  cvxpconn  31569  cvxsconn  31570  resconn  31573  iccllysconn  31577  noextendseq  32163  txpss3v  32328  txprel  32329  limitssson  32361  finminlem  32655  tailf  32713  filnetlem3  32718  onint1  32787  bj-unrab  33252  bj-2upln1upl  33341  bj-rrvecsscmn  33488  taupilem2  33504  taupi  33505  poimirlem3  33744  poimirlem30  33771  poimirlem31  33772  poimirlem32  33773  broucube  33775  opnmbllem0  33777  mblfinlem1  33778  mblfinlem2  33779  mblfinlem3  33780  mblfinlem4  33781  ismblfin  33782  mbfposadd  33788  cnambfre  33789  itg2addnc  33795  ftc1cnnclem  33814  ftc1cnnc  33815  ftc1anclem3  33818  ftc1anclem7  33822  ftc1anc  33824  ftc2nc  33825  dvreasin  33829  dvreacos  33830  areacirclem1  33831  areacirclem2  33832  areacirc  33836  caures  33886  reheibor  33968  xrnss3v  34466  xrnrel  34467  atlatmstc  35118  atlatle  35119  pmaple  35560  sspadd1  35614  sspadd2  35615  diophin  37856  4rexfrabdioph  37882  6rexfrabdioph  37883  irrapxlem1  37906  irrapx1  37912  monotuz  38025  jm2.27dlem5  38099  hbtlem2  38213  algbase  38267  algaddg  38268  algmulr  38269  algsca  38270  algvsca  38271  itgpowd  38318  arearect  38319  areaquad  38320  rtrclex  38442  trclubgNEW  38443  trclexi  38445  rtrclexi  38446  cnvtrcl0  38451  dfrtrcl5  38454  trrelsuperrel2dg  38481  relexpaddss  38528  brtrclfv2  38537  frege131d  38574  xphe  38593  idhe  38599  clsk3nimkb  38856  gneispace  38950  k0004val0  38970  lhe4.4ex1a  39046  uzmptshftfval  39063  binomcxplemdvbinom  39070  binomcxplemcvg  39071  binomcxplemnotnn0  39073  relopabVD  39649  fzisoeu  40013  fzsscn  40024  fzssre  40027  fzossuz  40096  fzossz  40097  uzssre  40117  zssxr  40118  uzssre2  40130  supminfxr  40191  uzsscn  40203  rpssxr  40208  ioosscn  40218  uzinico  40285  limcresiooub  40372  limcresioolb  40373  limcleqr  40374  limclner  40381  limclr  40385  limsupequzmpt2  40448  liminfval2  40498  liminfequzmpt2  40521  icccncfext  40598  cncficcgt0  40599  ioodvbdlimc1lem2  40645  ioodvbdlimc2lem  40647  dvnprodlem1  40659  dvnprodlem2  40660  itgsin0pilem1  40663  itgsinexplem1  40667  itgsinexp  40668  dirkercncflem2  40818  fourierdlem16  40837  fourierdlem18  40839  fourierdlem20  40841  fourierdlem21  40842  fourierdlem22  40843  fourierdlem25  40846  fourierdlem37  40858  fourierdlem42  40863  fourierdlem50  40870  fourierdlem52  40872  fourierdlem62  40882  fourierdlem64  40884  fourierdlem66  40886  fourierdlem68  40888  fourierdlem74  40894  fourierdlem75  40895  fourierdlem76  40896  fourierdlem79  40899  fourierdlem83  40903  fourierdlem95  40915  fourierdlem101  40921  fourierdlem102  40922  fourierdlem103  40923  fourierdlem104  40924  fourierdlem112  40932  fourierdlem114  40934  sqwvfoura  40942  sqwvfourb  40943  fouriersw  40945  etransclem24  40972  etransclem48  40996  sge0sn  41093  sge0tsms  41094  sge0f1o  41096  sge0pr  41108  sge0resplit  41120  sge0split  41123  sge0iunmptlemre  41129  sge0isummpt2  41146  carageniuncllem1  41235  hoicvr  41262  hoicvrrex  41270  hoidmvlelem2  41310  hspmbl  41343  smfmullem4  41501  prmdvdsfmtnof1lem1  42089  prmdvdsfmtnof  42091  oddibas  42399  2zrngbas  42522  2zrng0  42524  aacllem  43136  amgmlemALT  43138
  Copyright terms: Public domain W3C validator