![]() |
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 3034 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2anc 404 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3000 |
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 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-11 1443 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 |
This theorem depends on definitions: df-bi 116 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-in 3006 df-ss 3013 |
This theorem is referenced by: syl5ss 3037 syl6ss 3038 ssdif2d 3140 tfisi 4415 funss 5047 fssxp 5191 fvmptssdm 5400 suppssfv 5866 suppssov1 5867 tposss 6025 tfrlem1 6087 tfrlemibfn 6107 tfr1onlembfn 6123 tfr1onlemubacc 6125 tfr1onlemres 6128 tfrcllembfn 6136 tfrcllemubacc 6138 tfrcllemres 6141 ecinxp 6381 undifdc 6688 sbthlem1 6720 iseqf1olemnab 9978 isumss 10844 strsetsid 11588 strleund 11643 ntrss 11880 rescncf 11910 |
Copyright terms: Public domain | W3C validator |