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

Theorem sstri 3975
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 3973 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951
This theorem is referenced by:  snsstp1  4743  snsstp2  4744  uniintsn  4906  ssrnres  6029  cossxp  6117  foimacnv  6626  ssimaex  6742  riotassuni  7143  oprabss  7249  dmexg  7601  rnexg  7602  fabexg  7627  fparlem3  7800  fparlem4  7801  snopsuppss  7836  tposssxp  7887  mapsspw  8432  sbthlem5  8620  sbthlem7  8622  cnvimamptfin  8814  marypha1lem  8886  ordtypelem4  8974  hartogslem1  8995  tc2  9173  tz9.12lem1  9205  rankval4  9285  rankxpl  9293  rankmapu  9296  rankxplim  9297  djuin  9336  infxpenlem  9428  ackbij1lem18  9648  cflm  9661  fin23lem29  9752  hsmexlem4  9840  hsmexlem5  9841  brdom3  9939  brdom5  9940  brdom4  9941  smobeth  9997  pwfseqlem3  10071  wundm  10139  wunrn  10140  wunex2  10149  ltsopi  10299  dmaddpi  10301  dmmulpi  10302  nqerf  10341  ltrelxr  10691  uzwo2  12301  infssuzle  12320  infssuzcl  12321  uzwo3  12332  nn0ssq  12346  nnssq  12347  qsscn  12349  rpnnen1lem3  12368  rpnnen1lem5  12370  dflt2  12531  fzval2  12885  fzossz  13047  fzossnn  13076  injresinj  13148  flval3  13175  uzsup  13221  uzrdgfni  13316  expcl2lem  13431  rpexpcl  13438  expge0  13455  expge1  13456  hashxrcl  13708  seqcoll  13812  wrdexgOLD  13862  xptrrel  14330  trclublem  14345  sqrlem3  14594  limsupval2  14827  limsupgre  14828  rlimpm  14847  rlimclim  14893  isercolllem1  15011  isercolllem2  15012  isercoll  15014  caurcvg  15023  caucvg  15025  summolem2a  15062  summolem2  15063  zsum  15065  fsumcvg3  15076  fsumrpcl  15084  fsumge0  15140  climfsum  15165  ackbijnn  15173  prodmolem2a  15278  prodmolem2  15279  zprod  15281  fprodrpcl  15300  fprodge0  15337  fprodge1  15339  rprisefaccl  15367  divalglem8  15741  sadaddlem  15805  lcmfval  15955  isprm3  16017  maxprmfct  16043  pclem  16165  prmreclem1  16242  prmreclem2  16243  prmreclem3  16244  1arith  16253  4sqlem11  16281  ramtlecl  16326  ramcl2lem  16335  ramxrcl  16343  prmgaplem3  16379  prmgaplem4  16380  cshwshashlem1  16419  structfn  16490  strleun  16581  srngbase  16618  srngplusg  16619  srngmulr  16620  lmodbase  16627  lmodplusg  16628  lmodsca  16629  ipsbase  16634  ipsaddg  16635  ipsmulr  16636  ipssca  16637  ipsvsca  16638  ipsip  16639  phlbase  16644  phlplusg  16645  phlsca  16646  phlvsca  16647  phlip  16648  odrngbas  16670  odrngplusg  16671  odrngmulr  16672  odrngtset  16673  odrngle  16674  odrngds  16675  prdsval  16718  prdssca  16719  prdsbas  16720  prdsplusg  16721  prdsmulr  16722  prdsvsca  16723  prdsip  16724  prdsle  16725  prdsds  16727  prdstset  16729  prdshom  16730  prdsco  16731  imasbas  16775  imasds  16776  imasplusg  16780  imasmulr  16781  imassca  16782  imasvsca  16783  imasip  16784  imastset  16785  imasle  16786  wunfunc  17159  fullfunc  17166  fthfunc  17167  isfull  17170  isfth  17174  wunnat  17216  dmcoass  17316  catcisolem  17356  catciso  17357  catcoppccl  17358  catcfuccl  17359  catcxpccl  17447  ipobas  17755  ipolerval  17756  ipotset  17757  psdmrn  17807  psss  17814  ledm  17824  lern  17825  dirdm  17834  dirge  17837  mulgfval  18166  mvdco  18504  f1omvdconj  18505  gexex  18904  gsumval3  18958  lssacs  19670  asplss  20033  aspsubrg  20035  psrass1lem  20087  psrbas  20088  psrplusg  20091  psrmulr  20094  psrsca  20099  psrvscafval  20100  psrass1  20115  psrass23l  20118  psrcom  20119  psrass23  20120  psropprmul  20336  coe1mul2  20367  cnfldbas  20479  cnfldadd  20480  cnfldmul  20481  cnfldcj  20482  cnfldtset  20483  cnfldle  20484  cnfldds  20485  cnfldunif  20486  rge0srg  20546  zntoslem  20633  ofco2  20990  toponsspwpw  21460  dmtopon  21461  leordtval2  21750  lmbrf  21798  lmres  21838  fiuncmp  21942  comppfsc  22070  1stckgenlem  22091  kgencn3  22096  ptbasfi  22119  xkoopn  22127  txcnmpt  22162  txkgen  22190  opnfbas  22380  fmfnfmlem4  22495  tsmsxplem1  22690  trust  22767  restutop  22775  nmoffn  23249  nmofval  23252  nmogelb  23254  nmolb  23255  nmof  23257  qtopbas  23297  tgqioo  23337  re2ndc  23338  iitopon  23416  dfii3  23420  iimulcn  23471  cnheiborlem  23487  bndth  23491  lebnumii  23499  reparphti  23530  pcoass  23557  cphsqrtcl  23717  lmmbrf  23794  iscauf  23812  caucfil  23815  lmclimf  23836  rrxmval  23937  rrxmet  23940  ovolfioo  23997  ovolficc  23998  ovolficcss  23999  ovolfsf  24001  ovollb  24009  ovolicc2lem3  24049  ovolicc2lem4  24050  ovolicc2  24052  volf  24059  volsup  24086  ovolfs2  24101  uniiccdif  24108  uniioovol  24109  uniiccvol  24110  uniioombllem2  24113  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  uniioombl  24119  dyadmbllem  24129  dyadmbl  24130  opnmbllem  24131  opnmblALT  24133  volsup2  24135  vitalilem4  24141  vitalilem5  24142  vitali  24143  mbfimaopnlem  24185  mbflimsup  24196  i1f0  24217  i1f1  24220  itg11  24221  itg2mulc  24277  itg2gt0  24290  ellimc2  24404  limcresi  24412  dvreslem  24436  dvres2lem  24437  dvaddbr  24464  dvmulbr  24465  dvlipcn  24520  c1liplem1  24522  lhop1lem  24539  lhop1  24540  lhop2  24541  lhop  24542  dvfsumrlim  24557  ftc1cn  24569  itgsubstlem  24574  itgsubst  24575  mdegleb  24587  mdeglt  24588  mdegldg  24589  mdegxrcl  24590  mdegcl  24592  mdegaddle  24597  mdegmullem  24601  deg1mul3le  24639  ig1peu  24694  ig1pdvds  24699  aacjcl  24845  aannenlem2  24847  aannenlem3  24848  aalioulem2  24851  taylfval  24876  radcnvcl  24934  radcnvlt1  24935  radcnvle  24937  abelth  24958  abelth2  24959  pilem2  24969  pilem3  24970  pige3ALT  25034  recosf1o  25046  resinf1o  25047  tanord1  25048  logcn  25157  dvlog  25161  dvlog2lem  25162  efopn  25168  logtayl  25170  cxpcn3  25256  loglesqrt  25266  ssscongptld  25327  leibpi  25448  efrlim  25475  jensenlem1  25492  jensenlem2  25493  jensen  25494  amgm  25496  lgamgulmlem2  25535  ftalem5  25582  efnnfsumcl  25608  efchtdvds  25664  dvdsmulf1o  25699  fsumdvdsmul  25700  lgsfcl2  25807  2sqlem6  25927  2sqlem8  25930  2sqlem9  25931  rpvmasumlem  25991  rpvmasum2  26016  dchrisum0re  26017  dchrisum0lem3  26023  dchrisum0  26024  rplogsum  26031  dirith2  26032  axtgcgrrflx  26176  axtgcgrid  26177  axtgsegcon  26178  axtg5seg  26179  axtgbtwnid  26180  axtgpasch  26181  axtgcont1  26182  tgcgr4  26245  motcgrg  26258  tglng  26260  upgrss  26801  pthdivtx  27438  disjxwwlkn  27620  ex-fpar  28169  nmlno0lem  28498  hlimcaui  28941  chsspwh  28952  shsss  29018  chintcli  29036  shsleji  29075  shub1i  29079  shsval2i  29092  lejdii  29243  spanuni  29249  sshhococi  29251  spansnpji  29283  osumcori  29348  5oai  29366  3oalem6  29372  3oai  29373  pjssmii  29386  mayete3i  29433  mayetes3i  29434  nmlnop0iALT  29700  imaelshi  29763  pjnmopi  29853  pjclem1  29900  pjci  29905  mdslmd1lem1  30030  shatomistici  30066  hatomistici  30067  chpssati  30068  xppreima  30323  iundisjfi  30446  iundisj2fi  30447  fprodex01  30469  xrsmulgzz  30593  fsumrp0cl  30610  gsummpt2co  30614  cycpmfv2  30684  cycpmrn  30713  xrge0slmod  30845  unitsscn  31039  ordtconnlem1  31067  xrge0iifhom  31080  lmlimxrge0  31091  lmxrge0  31095  indsumin  31181  esumcst  31222  esumpfinvallem  31233  esumpfinval  31234  esumpfinvalf  31235  esumcvg  31245  imambfm  31420  elmbfmvol2  31425  sxbrsigalem3  31430  sxbrsigalem2  31444  sxbrsigalem4  31445  sitgclg  31500  eulerpartlem1  31525  eulerpartlemgvv  31534  eulerpartlemgh  31536  eulerpartlemgf  31537  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemiex  31659  ballotlemsup  31662  ballotlemsdom  31669  ballotlemsima  31673  ballotlemrv2  31679  ballotth  31695  signsplypnf  31720  signsply0  31721  rpsqrtcn  31764  itgexpif  31777  fsum2dsub  31778  reprfi2  31794  chtvalz  31800  breprexplemc  31803  breprexpnat  31805  circlemeth  31811  circlemethnat  31812  circlevma  31813  circlemethhgt  31814  hgt750lemd  31819  hgt750lema  31828  tgoldbachgtde  31831  tgoldbachgtda  31832  tgoldbachgt  31834  bnj1145  32163  bnj1286  32189  subfacp1lem2a  32325  erdszelem4  32339  erdszelem5  32340  erdszelem7  32342  erdszelem8  32343  kur14lem7  32357  kur14lem9  32359  cvxpconn  32387  cvxsconn  32388  resconn  32391  iccllysconn  32395  noextendseq  33072  txpss3v  33237  txprel  33238  limitssson  33270  finminlem  33564  tailf  33621  filnetlem3  33626  onint1  33695  bj-unrab  34142  bj-2upln1upl  34234  bj-rvecssabl  34476  taupilem2  34486  taupi  34487  poimirlem3  34777  poimirlem30  34804  poimirlem31  34805  poimirlem32  34806  broucube  34808  opnmbllem0  34810  mblfinlem1  34811  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  mbfposadd  34821  cnambfre  34822  itg2addnc  34828  ftc1cnnclem  34847  ftc1cnnc  34848  ftc1anclem3  34851  ftc1anclem7  34855  ftc1anc  34857  ftc2nc  34858  dvreasin  34862  dvreacos  34863  areacirclem1  34864  areacirclem2  34865  areacirc  34869  caures  34918  reheibor  35000  xrnss3v  35506  xrnrel  35507  atlatmstc  36337  atlatle  36338  pmaple  36779  sspadd1  36833  sspadd2  36834  diophin  39249  4rexfrabdioph  39275  6rexfrabdioph  39276  irrapxlem1  39299  irrapx1  39305  monotuz  39418  jm2.27dlem5  39490  hbtlem2  39604  algbase  39658  algaddg  39659  algmulr  39660  algsca  39661  algvsca  39662  itgpowd  39701  arearect  39702  areaquad  39703  rtrclex  39857  trclubgNEW  39858  trclexi  39860  rtrclexi  39861  cnvtrcl0  39866  dfrtrcl5  39869  trrelsuperrel2dg  39896  relexpaddss  39943  brtrclfv2  39952  frege131d  39989  xphe  40007  clsk3nimkb  40270  gneispace  40364  k0004val0  40384  inaex  40513  lhe4.4ex1a  40541  uzmptshftfval  40558  binomcxplemdvbinom  40565  binomcxplemcvg  40566  binomcxplemnotnn0  40568  relopabVD  41115  fzisoeu  41447  fzsscn  41458  fzssre  41461  fzossuz  41530  uzssre  41549  zssxr  41550  uzssre2  41560  supminfxr  41620  uzsscn  41632  rpssxr  41637  ioosscn  41649  uzinico  41716  limcresiooub  41803  limcresioolb  41804  limcleqr  41805  limclner  41812  limclr  41816  limsupequzmpt2  41879  liminfval2  41929  liminfequzmpt2  41952  icccncfext  42050  cncficcgt0  42051  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnprodlem1  42111  dvnprodlem2  42112  itgsin0pilem1  42115  itgsinexplem1  42119  itgsinexp  42120  dirkercncflem2  42270  fourierdlem16  42289  fourierdlem18  42291  fourierdlem20  42293  fourierdlem21  42294  fourierdlem22  42295  fourierdlem25  42298  fourierdlem37  42310  fourierdlem42  42315  fourierdlem50  42322  fourierdlem52  42324  fourierdlem62  42334  fourierdlem64  42336  fourierdlem66  42338  fourierdlem68  42340  fourierdlem74  42346  fourierdlem75  42347  fourierdlem76  42348  fourierdlem79  42351  fourierdlem83  42355  fourierdlem95  42367  fourierdlem101  42373  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem112  42384  fourierdlem114  42386  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  etransclem24  42424  etransclem48  42448  sge0sn  42542  sge0tsms  42543  sge0f1o  42545  sge0pr  42557  sge0resplit  42569  sge0split  42572  sge0iunmptlemre  42578  sge0isummpt2  42595  carageniuncllem1  42684  hoicvr  42711  hoicvrrex  42719  hoidmvlelem2  42759  hspmbl  42792  smfmullem4  42950  prmdvdsfmtnof1lem1  43593  prmdvdsfmtnof  43595  oddibas  43927  2zrngbas  44105  2zrng0  44107  aacllem  44800  amgmlemALT  44802
  Copyright terms: Public domain W3C validator