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 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
syl6ss.2 | ⊢ 𝐵 ⊆ 𝐶 |
Ref | Expression |
---|---|
syl6ss | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6ss.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | syl6ss.2 | . . 3 ⊢ 𝐵 ⊆ 𝐶 | |
3 | 2 | a1i 9 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
4 | 1, 3 | sstrd 2955 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 2917 |
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 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-in 2924 df-ss 2931 |
This theorem is referenced by: difss2 3072 sstpr 3528 rintm 3744 eqbrrdva 4505 ssxpbm 4756 ssxp1 4757 ssxp2 4758 relfld 4846 funssxp 5060 dff2 5311 fliftf 5439 1stcof 5790 2ndcof 5791 tfrlemibfn 5942 sucinc2 6026 peano5nnnn 6966 peano5nni 7917 ioodisj 8861 fzossnn0 9031 elfzom1elp1fzo 9058 frecuzrdgfn 9198 peano5set 10064 peano5setOLD 10065 |
Copyright terms: Public domain | W3C validator |