Theorem sstr 2068

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 2067	. 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 2043

This theorem is referenced by:  sstrd 2070  ssdifss 2164  uneqin 2252  sspwuni 2753  ssrnres 3473  funssxp 3629  fssres 3634  ssimaex 3759  dff4 3807  dff2 3808  om00 4196  mapval2 4325  unblem1 4523  unblem2 4524  unblem3 4525  unblem4 4526  isfinite2 4529  rankr1b 4679  rankxplim3 4694  fodom 4778  supxrbnd 6046  supxrgtmnf 6047  supxrre1 6048  supxrre2 6049  uzwo4OLD 6166  uzwo5OLD 6167  iccsupr 6339  uzwo 6395  uzwoOLD 6396  uzwo2 6397  infmssuzle 6405  infmssuzcl 6406  rescncf 7215  infxpidmlem11 7513  tgvalt 7566  unitgt 7573  tgval3t 7575  tgss2t 7587  basgen2t 7589  fctop 7600  cctop 7602  ssnei 7674  opnneiss 7682  cnpco 7719  blssex 7806  opnin 7821  metcnp 7839  lmbrf 7882  iscauf 7891  iscau5 7893  lmsslem 7903  caussi 7905  lmclimnn 7915  bcthlem16 7964  nmoge0 8375  ubthlem6 8478  h2hcau 8788  h2hlm 8789  shsupunss 9253  chsupunss 9254  spanss 9256  shlub 9284  shslub 9296  shmod 9301  mdslj1 10183  mdsl1 10185  mdsl2 10186  cvmd 10188  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd2 10194  mdslmd4 10197  atoml 10246  atcvatlem 10249  irredlem2 10255  irred 10258  mdsymlem5 10271  fgsb 10480  efilcp 10481  fisub 10483  fgsb2 10485  efilcp2 10486

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain