![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sstrd | GIF 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 3163 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2anc 411 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3129 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: sstrid 3166 sstrdi 3167 ssdif2d 3274 tfisi 4586 funss 5235 fssxp 5383 fvmptssdm 5600 suppssfv 6078 suppssov1 6079 tposss 6246 tfrlem1 6308 tfrlemibfn 6328 tfr1onlembfn 6344 tfr1onlemubacc 6346 tfr1onlemres 6349 tfrcllembfn 6357 tfrcllemubacc 6359 tfrcllemres 6362 ecinxp 6609 undifdc 6922 sbthlem1 6955 iseqf1olemnab 10485 fiubm 10803 isumss 11394 prodssdc 11592 ennnfoneleminc 12406 strsetsid 12489 strleund 12556 strext 12558 imasaddvallemg 12718 subsubg 13010 subgintm 13011 subsubrg 13326 ntrss 13512 neiint 13538 neiss 13543 restopnb 13574 iscnp4 13611 blssps 13820 blss 13821 xmettx 13903 tgqioo 13940 rescncf 13961 suplociccreex 13995 suplociccex 13996 dvbss 14047 dvbsssg 14048 dvfgg 14050 dvcnp2cntop 14056 dvcn 14057 dvaddxxbr 14058 dvmulxxbr 14059 dvcoapbr 14064 |
Copyright terms: Public domain | W3C validator |