Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sstr | Unicode version |
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.) |
Ref | Expression |
---|---|
sstr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstr2 3074 | . 2 | |
2 | 1 | imp 123 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wss 3041 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: sstrd 3077 sylan9ss 3080 ssdifss 3176 uneqin 3297 ssindif0im 3392 undifss 3413 ssrnres 4951 relrelss 5035 fco 5258 fssres 5268 ssimaex 5450 tpostpos2 6130 smores 6157 pmss12g 6537 fidcenumlemr 6811 iccsupr 9717 fimaxq 10541 fsum2d 11172 fsumabs 11202 tgval 12145 tgvalex 12146 ssnei 12247 opnneiss 12254 restdis 12280 tgcnp 12305 blssexps 12525 blssex 12526 mopni3 12580 metss 12590 metcnp3 12607 tgioo 12642 cncfmptid 12679 |
Copyright terms: Public domain | W3C validator |