![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sstrd | Unicode version |
Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.) |
Ref | Expression |
---|---|
sstrd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sstrd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sstrd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstrd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sstrd.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | sstr 3071 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2anc 406 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-11 1467 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-in 3043 df-ss 3050 |
This theorem is referenced by: sstrid 3074 syl6ss 3075 ssdif2d 3181 tfisi 4461 funss 5100 fssxp 5248 fvmptssdm 5459 suppssfv 5932 suppssov1 5933 tposss 6097 tfrlem1 6159 tfrlemibfn 6179 tfr1onlembfn 6195 tfr1onlemubacc 6197 tfr1onlemres 6200 tfrcllembfn 6208 tfrcllemubacc 6210 tfrcllemres 6213 ecinxp 6458 undifdc 6765 sbthlem1 6797 iseqf1olemnab 10154 isumss 11052 ennnfoneleminc 11769 strsetsid 11835 strleund 11890 ntrss 12131 neiint 12157 neiss 12162 restopnb 12193 iscnp4 12229 blssps 12416 blss 12417 xmettx 12499 tgqioo 12533 rescncf 12554 dvbss 12609 dvbsssg 12610 dvfgg 12612 dvcnp2cntop 12618 dvcn 12619 dvaddxxbr 12620 dvmulxxbr 12621 |
Copyright terms: Public domain | W3C validator |