![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6ss | GIF version |
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
syl6ss.1 | ⊢ (φ → A ⊆ B) |
syl6ss.2 | ⊢ B ⊆ 𝐶 |
Ref | Expression |
---|---|
syl6ss | ⊢ (φ → A ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6ss.1 | . 2 ⊢ (φ → A ⊆ B) | |
2 | syl6ss.2 | . . 3 ⊢ B ⊆ 𝐶 | |
3 | 2 | a1i 9 | . 2 ⊢ (φ → B ⊆ 𝐶) |
4 | 1, 3 | sstrd 2949 | 1 ⊢ (φ → A ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 2911 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-11 1394 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-in 2918 df-ss 2925 |
This theorem is referenced by: difss2 3066 sstpr 3519 rintm 3735 eqbrrdva 4448 ssxpbm 4699 ssxp1 4700 ssxp2 4701 relfld 4789 funssxp 5003 dff2 5254 fliftf 5382 1stcof 5732 2ndcof 5733 tfrlemibfn 5883 sucinc2 5965 peano5nni 7698 ioodisj 8631 fzossnn0 8801 elfzom1elp1fzo 8828 frecuzrdgfn 8879 peano5set 9399 peano5setOLD 9400 |
Copyright terms: Public domain | W3C validator |