Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssidd | GIF version |
Description: Weakening of ssid 3157. (Contributed by BJ, 1-Sep-2022.) |
Ref | Expression |
---|---|
ssidd | ⊢ (𝜑 → 𝐴 ⊆ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid 3157 | . 2 ⊢ 𝐴 ⊆ 𝐴 | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3111 |
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 3117 df-ss 3124 |
This theorem is referenced by: isum 11312 fsum3ser 11324 fsumcl 11327 iprodap 11507 iprodap0 11509 fprodssdc 11517 fprodcl 11534 fprodclf 11562 ennnfoneleminc 12287 restopn2 12730 negcncf 13135 mulcncf 13138 dvidlemap 13207 dvaddxxbr 13212 dvmulxxbr 13213 dvcoapbr 13218 dvcjbr 13219 dvexp 13222 dvrecap 13224 dvmptcmulcn 13230 dvmptnegcn 13231 dvmptsubcn 13232 dveflem 13234 dvef 13235 bj-charfundcALT 13532 |
Copyright terms: Public domain | W3C validator |