Theorem sstr 2072

Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23.

Assertion

Ref	Expression
sstr	|- ((A (_ B /\ B (_ C) -> A (_ C)

Proof of Theorem sstr

Step	Hyp	Ref	Expression
1		sstr2 2071	. 2 |- (A (_ B -> (B (_ C -> A (_ C))
2	1	imp 350	1 |- ((A (_ B /\ B (_ C) -> A (_ C)

Syntax hints:   -> wi 3   /\ wa 223   (_ wss 2047

This theorem is referenced by:  sstrd 2074  ssdifss 2168  uneqin 2256  sspwuni 2758  ssrnres 3481  funssxp 3638  fssres 3643  ssimaex 3768  dff4 3816  dff2 3817  om00 4206  mapval2 4335  unblem1 4540  unblem2 4541  unblem3 4542  unblem4 4543  isfinite2OLD 4546  rankr1b 4699  rankxplim3 4714  fodom 4798  supxrbnd 6091  supxrgtmnf 6092  supxrre1 6093  supxrre2 6094  uzwo4OLD 6210  uzwo5OLD 6211  iccsupr 6398  uzwo 6455  uzwoOLD 6456  uzwo2 6457  infmssuzle 6465  infmssuzcl 6466  rescncf 7272  infxpidmlem11 7562  tgvalt 7616  unitgt 7623  tgval3t 7625  tgss2t 7637  basgen2t 7639  fctopOLD 7650  cctop 7652  ssnei 7724  opnneiss 7732  cnpco 7769  blssex 7854  opnin 7869  metcnp 7887  lmbrf 7930  iscauf 7939  iscau5 7941  iscaunns 7944  lmsslem 7952  caussi 7954  lmclimnn 7964  bcthlem16 8014  nmoge0 8430  ubthlem6 8534  h2hcau 8849  h2hlm 8850  shsupunss 9315  chsupunss 9316  spanss 9318  shlub 9346  shslub 9358  shmod 9363  mdslj1 10246  mdsl1 10248  mdsl2 10249  cvmd 10251  mdslmd1lem1 10252  mdslmd1lem2 10253  mdslmd2 10257  mdslmd4 10260  atoml 10309  atcvatlem 10312  irredlem2 10318  irred 10321  mdsymlem5 10334  top2usne 10549  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  fisub 10576  fisubOLD 10577  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain