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

Theorem sstri 3927
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 3925 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 9 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  snsstp1  4712  snsstp2  4713  uniintsn  4878  ssrnres  6006  cossxp  6095  foimacnv  6611  ssimaex  6727  riotassuni  7137  oprabss  7243  dmexg  7598  rnexg  7599  fabexg  7625  fparlem3  7796  fparlem4  7797  snopsuppss  7832  tposssxp  7883  mapsspw  8429  sbthlem5  8619  sbthlem7  8621  cnvimamptfin  8813  marypha1lem  8885  ordtypelem4  8973  hartogslem1  8994  tc2  9172  tz9.12lem1  9204  rankval4  9284  rankxpl  9292  rankmapu  9295  rankxplim  9296  djuin  9335  infxpenlem  9428  ackbij1lem18  9652  cflm  9665  fin23lem29  9756  hsmexlem4  9844  hsmexlem5  9845  brdom3  9943  brdom5  9944  brdom4  9945  smobeth  10001  pwfseqlem3  10075  wundm  10143  wunrn  10144  wunex2  10153  ltsopi  10303  dmaddpi  10305  dmmulpi  10306  nqerf  10345  ltrelxr  10695  uzwo2  12304  infssuzle  12323  infssuzcl  12324  uzwo3  12335  nn0ssq  12348  nnssq  12349  qsscn  12351  rpnnen1lem3  12370  rpnnen1lem5  12372  dflt2  12533  ioosscn  12791  unitsscn  12882  fzval2  12892  fzossz  13056  fzossnn  13085  injresinj  13157  flval3  13184  uzsup  13230  uzrdgfni  13325  expcl2lem  13441  rpexpcl  13448  expge0  13465  expge1  13466  hashxrcl  13718  seqcoll  13822  xptrrel  14335  trclublem  14350  sqrlem3  14600  limsupval2  14833  limsupgre  14834  rlimpm  14853  rlimclim  14899  isercolllem1  15017  isercolllem2  15018  isercoll  15020  caurcvg  15029  caucvg  15031  summolem2a  15068  summolem2  15069  zsum  15071  fsumcvg3  15082  fsumrpcl  15090  fsumge0  15146  climfsum  15171  ackbijnn  15179  prodmolem2a  15284  prodmolem2  15285  zprod  15287  fprodrpcl  15306  fprodge0  15343  fprodge1  15345  rprisefaccl  15373  divalglem8  15745  sadaddlem  15809  lcmfval  15959  isprm3  16021  maxprmfct  16047  pclem  16169  prmreclem1  16246  prmreclem2  16247  prmreclem3  16248  1arith  16257  4sqlem11  16285  ramtlecl  16330  ramcl2lem  16339  ramxrcl  16347  prmgaplem3  16383  prmgaplem4  16384  cshwshashlem1  16425  structfn  16496  strleun  16587  srngbase  16624  srngplusg  16625  srngmulr  16626  lmodbase  16633  lmodplusg  16634  lmodsca  16635  ipsbase  16640  ipsaddg  16641  ipsmulr  16642  ipssca  16643  ipsvsca  16644  ipsip  16645  phlbase  16650  phlplusg  16651  phlsca  16652  phlvsca  16653  phlip  16654  odrngbas  16676  odrngplusg  16677  odrngmulr  16678  odrngtset  16679  odrngle  16680  odrngds  16681  prdsval  16724  prdssca  16725  prdsbas  16726  prdsplusg  16727  prdsmulr  16728  prdsvsca  16729  prdsip  16730  prdsle  16731  prdsds  16733  prdstset  16735  prdshom  16736  prdsco  16737  imasbas  16781  imasds  16782  imasplusg  16786  imasmulr  16787  imassca  16788  imasvsca  16789  imasip  16790  imastset  16791  imasle  16792  wunfunc  17165  fullfunc  17172  fthfunc  17173  isfull  17176  isfth  17180  wunnat  17222  dmcoass  17322  catcisolem  17362  catciso  17363  catcoppccl  17364  catcfuccl  17365  catcxpccl  17453  ipobas  17761  ipolerval  17762  ipotset  17763  psdmrn  17813  psss  17820  ledm  17830  lern  17831  dirdm  17840  dirge  17843  mulgfval  18222  mvdco  18569  f1omvdconj  18570  gexex  18970  gsumval3  19024  lssacs  19736  cnfldbas  20099  cnfldadd  20100  cnfldmul  20101  cnfldcj  20102  cnfldtset  20103  cnfldle  20104  cnfldds  20105  cnfldunif  20106  rge0srg  20166  zntoslem  20252  asplss  20564  aspsubrg  20566  psrass1lem  20619  psrbas  20620  psrplusg  20623  psrmulr  20626  psrsca  20631  psrvscafval  20632  psrass1  20647  psrass23l  20650  psrcom  20651  psrass23  20652  psropprmul  20871  coe1mul2  20902  ofco2  21060  toponsspwpw  21531  dmtopon  21532  leordtval2  21821  lmbrf  21869  lmres  21909  fiuncmp  22013  comppfsc  22141  1stckgenlem  22162  kgencn3  22167  ptbasfi  22190  xkoopn  22198  txcnmpt  22233  txkgen  22261  opnfbas  22451  fmfnfmlem4  22566  tsmsxplem1  22762  trust  22839  restutop  22847  nmoffn  23321  nmofval  23324  nmogelb  23326  nmolb  23327  nmof  23329  qtopbas  23369  tgqioo  23409  re2ndc  23410  iitopon  23488  dfii3  23492  iimulcn  23547  cnheiborlem  23563  bndth  23567  lebnumii  23575  reparphti  23606  pcoass  23633  cphsqrtcl  23793  lmmbrf  23870  iscauf  23888  caucfil  23891  lmclimf  23912  rrxmval  24013  rrxmet  24016  ovolfioo  24075  ovolficc  24076  ovolficcss  24077  ovolfsf  24079  ovollb  24087  ovolicc2lem3  24127  ovolicc2lem4  24128  ovolicc2  24130  volf  24137  volsup  24164  ovolfs2  24179  uniiccdif  24186  uniioovol  24187  uniiccvol  24188  uniioombllem2  24191  uniioombllem3a  24192  uniioombllem3  24193  uniioombllem4  24194  uniioombllem5  24195  uniioombl  24197  dyadmbllem  24207  dyadmbl  24208  opnmbllem  24209  opnmblALT  24211  volsup2  24213  vitalilem4  24219  vitalilem5  24220  vitali  24221  mbfimaopnlem  24263  mbflimsup  24274  i1f0  24295  i1f1  24298  itg11  24299  itg2mulc  24355  itg2gt0  24368  ellimc2  24484  limcresi  24492  dvreslem  24516  dvres2lem  24517  dvaddbr  24545  dvmulbr  24546  dvlipcn  24601  c1liplem1  24603  lhop1lem  24620  lhop1  24621  lhop2  24622  lhop  24623  dvfsumrlim  24638  ftc1cn  24650  itgsubstlem  24655  itgsubst  24656  itgpowd  24657  mdegleb  24669  mdeglt  24670  mdegldg  24671  mdegxrcl  24672  mdegcl  24674  mdegaddle  24679  mdegmullem  24683  deg1mul3le  24721  ig1peu  24776  ig1pdvds  24781  aacjcl  24927  aannenlem2  24929  aannenlem3  24930  aalioulem2  24933  taylfval  24958  radcnvcl  25016  radcnvlt1  25017  radcnvle  25019  abelth  25040  abelth2  25041  pilem2  25051  pilem3  25052  pige3ALT  25116  recosf1o  25131  resinf1o  25132  tanord1  25133  logcn  25242  dvlog  25246  dvlog2lem  25247  efopn  25253  logtayl  25255  cxpcn3  25341  loglesqrt  25351  ssscongptld  25412  leibpi  25532  efrlim  25559  jensenlem1  25576  jensenlem2  25577  jensen  25578  amgm  25580  lgamgulmlem2  25619  ftalem5  25666  efnnfsumcl  25692  efchtdvds  25748  dvdsmulf1o  25783  fsumdvdsmul  25784  lgsfcl2  25891  2sqlem6  26011  2sqlem8  26014  2sqlem9  26015  rpvmasumlem  26075  rpvmasum2  26100  dchrisum0re  26101  dchrisum0lem3  26107  dchrisum0  26108  rplogsum  26115  dirith2  26116  axtgcgrrflx  26260  axtgcgrid  26261  axtgsegcon  26262  axtg5seg  26263  axtgbtwnid  26264  axtgpasch  26265  axtgcont1  26266  tgcgr4  26329  motcgrg  26342  tglng  26344  upgrss  26885  pthdivtx  27522  disjxwwlkn  27703  ex-fpar  28251  nmlno0lem  28580  hlimcaui  29023  chsspwh  29034  shsss  29100  chintcli  29118  shsleji  29157  shub1i  29161  shsval2i  29174  lejdii  29325  spanuni  29331  sshhococi  29333  spansnpji  29365  osumcori  29430  5oai  29448  3oalem6  29454  3oai  29455  pjssmii  29468  mayete3i  29515  mayetes3i  29516  nmlnop0iALT  29782  imaelshi  29845  pjnmopi  29935  pjclem1  29982  pjci  29987  mdslmd1lem1  30112  shatomistici  30148  hatomistici  30149  chpssati  30150  xppreima  30412  iundisjfi  30549  iundisj2fi  30550  fprodex01  30571  xrsmulgzz  30716  fsumrp0cl  30733  gsummpt2co  30737  cycpmfv2  30810  cycpmrn  30839  xrge0slmod  30972  lsmsnorb  31003  idlsrgbas  31061  idlsrgplusg  31062  idlsrgmulr  31064  idlsrgtset  31065  ordtconnlem1  31281  xrge0iifhom  31294  lmlimxrge0  31305  lmxrge0  31309  indsumin  31395  esumcst  31436  esumpfinvallem  31447  esumpfinval  31448  esumpfinvalf  31449  esumcvg  31459  imambfm  31634  elmbfmvol2  31639  sxbrsigalem3  31644  sxbrsigalem2  31658  sxbrsigalem4  31659  sitgclg  31714  eulerpartlem1  31739  eulerpartlemgvv  31748  eulerpartlemgh  31750  eulerpartlemgf  31751  ballotlemfc0  31864  ballotlemfcc  31865  ballotlemiex  31873  ballotlemsup  31876  ballotlemsdom  31883  ballotlemsima  31887  ballotlemrv2  31893  ballotth  31909  signsplypnf  31934  signsply0  31935  rpsqrtcn  31978  itgexpif  31991  fsum2dsub  31992  reprfi2  32008  chtvalz  32014  breprexplemc  32017  breprexpnat  32019  circlemeth  32025  circlemethnat  32026  circlevma  32027  circlemethhgt  32028  hgt750lemd  32033  hgt750lema  32042  tgoldbachgtde  32045  tgoldbachgtda  32046  tgoldbachgt  32048  bnj1145  32379  bnj1286  32405  subfacp1lem2a  32541  erdszelem4  32555  erdszelem5  32556  erdszelem7  32558  erdszelem8  32559  kur14lem7  32573  kur14lem9  32575  cvxpconn  32603  cvxsconn  32604  resconn  32607  iccllysconn  32611  noextendseq  33288  txpss3v  33453  txprel  33454  limitssson  33486  finminlem  33780  tailf  33837  filnetlem3  33842  onint1  33911  bj-unrab  34369  bj-2upln1upl  34461  bj-imdirco  34606  bj-rvecssabl  34721  taupilem2  34737  taupi  34738  poimirlem3  35059  poimirlem30  35086  poimirlem31  35087  poimirlem32  35088  broucube  35090  opnmbllem0  35092  mblfinlem1  35093  mblfinlem2  35094  mblfinlem3  35095  mblfinlem4  35096  ismblfin  35097  mbfposadd  35103  cnambfre  35104  itg2addnc  35110  ftc1cnnclem  35127  ftc1cnnc  35128  ftc1anclem3  35131  ftc1anclem7  35135  ftc1anc  35137  ftc2nc  35138  dvreasin  35142  dvreacos  35143  areacirclem1  35144  areacirclem2  35145  areacirc  35149  caures  35197  reheibor  35276  xrnss3v  35783  xrnrel  35784  atlatmstc  36614  atlatle  36615  pmaple  37056  sspadd1  37110  sspadd2  37111  diophin  39710  4rexfrabdioph  39736  6rexfrabdioph  39737  irrapxlem1  39760  irrapx1  39766  monotuz  39879  jm2.27dlem5  39951  hbtlem2  40065  algbase  40119  algaddg  40120  algmulr  40121  algsca  40122  algvsca  40123  arearect  40162  areaquad  40163  rtrclex  40314  trclubgNEW  40315  trclexi  40317  rtrclexi  40318  cnvtrcl0  40323  dfrtrcl5  40326  trrelsuperrel2dg  40369  relexpaddss  40416  brtrclfv2  40425  frege131d  40462  xphe  40479  clsk3nimkb  40740  gneispace  40834  k0004val0  40854  inaex  41002  lhe4.4ex1a  41030  uzmptshftfval  41047  binomcxplemdvbinom  41054  binomcxplemcvg  41055  binomcxplemnotnn0  41057  relopabVD  41604  fzisoeu  41929  fzsscn  41940  fzssre  41943  fzossuz  42011  uzssre  42030  zssxr  42031  uzssre2  42041  supminfxr  42100  uzsscn  42112  rpssxr  42117  uzinico  42194  limcresiooub  42281  limcresioolb  42282  limcleqr  42283  limclner  42290  limclr  42294  limsupequzmpt2  42357  liminfval2  42407  liminfequzmpt2  42430  icccncfext  42526  cncficcgt0  42527  ioodvbdlimc1lem2  42571  ioodvbdlimc2lem  42573  dvnprodlem1  42585  dvnprodlem2  42586  itgsin0pilem1  42589  itgsinexplem1  42593  itgsinexp  42594  dirkercncflem2  42743  fourierdlem16  42762  fourierdlem18  42764  fourierdlem20  42766  fourierdlem21  42767  fourierdlem22  42768  fourierdlem25  42771  fourierdlem37  42783  fourierdlem42  42788  fourierdlem50  42795  fourierdlem52  42797  fourierdlem62  42807  fourierdlem64  42809  fourierdlem66  42811  fourierdlem68  42813  fourierdlem74  42819  fourierdlem75  42820  fourierdlem76  42821  fourierdlem79  42824  fourierdlem83  42828  fourierdlem95  42840  fourierdlem101  42846  fourierdlem102  42847  fourierdlem103  42848  fourierdlem104  42849  fourierdlem112  42857  fourierdlem114  42859  sqwvfoura  42867  sqwvfourb  42868  fouriersw  42870  etransclem24  42897  etransclem48  42921  sge0sn  43015  sge0tsms  43016  sge0f1o  43018  sge0pr  43030  sge0resplit  43042  sge0split  43045  sge0iunmptlemre  43051  sge0isummpt2  43068  carageniuncllem1  43157  hoicvr  43184  hoicvrrex  43192  hoidmvlelem2  43232  hspmbl  43265  smfmullem4  43423  prmdvdsfmtnof1lem1  44098  prmdvdsfmtnof  44100  oddibas  44430  2zrngbas  44557  2zrng0  44559  aacllem  45326  amgmlemALT  45328
  Copyright terms: Public domain W3C validator