Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sstrid | GIF version |
Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.) |
Ref | Expression |
---|---|
sstrid.1 | ⊢ 𝐴 ⊆ 𝐵 |
sstrid.2 | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Ref | Expression |
---|---|
sstrid | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sstrid.1 | . . 3 ⊢ 𝐴 ⊆ 𝐵 | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
3 | sstrid.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | |
4 | 2, 3 | sstrd 3148 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3112 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3118 df-ss 3125 |
This theorem is referenced by: cossxp2 5122 fimacnv 5609 smores2 6254 f1imaen2g 6751 phplem4dom 6820 isinfinf 6855 fidcenumlemrk 6911 casef 7045 genipv 7442 fzossnn0 10101 seq3split 10405 ctinf 12317 nninfdclemcl 12335 nninfdclemp1 12337 tgcl 12622 epttop 12648 ntrin 12682 cnconst2 12791 cnrest2 12794 cnptopresti 12796 cnptoprest2 12798 hmeores 12873 blin2 12990 ivthdec 13180 limcdifap 13189 limcresi 13193 dvfgg 13215 dvcnp2cntop 13221 dvaddxxbr 13223 reeff1olem 13250 |
Copyright terms: Public domain | W3C validator |