ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sstr Unicode version

Theorem sstr 3105
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
Assertion
Ref Expression
sstr  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )

Proof of Theorem sstr
StepHypRef Expression
1 sstr2 3104 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 123 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    C_ wss 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  sstrd  3107  sylan9ss  3110  ssdifss  3206  uneqin  3327  ssindif0im  3422  undifss  3443  ssrnres  4981  relrelss  5065  fco  5288  fssres  5298  ssimaex  5482  tpostpos2  6162  smores  6189  pmss12g  6569  fidcenumlemr  6843  iccsupr  9756  fimaxq  10580  fsum2d  11211  fsumabs  11241  tgval  12228  tgvalex  12229  ssnei  12330  opnneiss  12337  restdis  12363  tgcnp  12388  blssexps  12608  blssex  12609  mopni3  12663  metss  12673  metcnp3  12690  tgioo  12725  cncfmptid  12762
  Copyright terms: Public domain W3C validator