![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqsstrid | GIF version |
Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Ref | Expression |
---|---|
eqsstrid.1 | ⊢ 𝐴 = 𝐵 |
eqsstrid.2 | ⊢ (𝜑 → 𝐵 ⊆ 𝐶) |
Ref | Expression |
---|---|
eqsstrid | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqsstrid.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶) | |
2 | eqsstrid.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 2 | sseq1i 3128 | . 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
4 | 1, 3 | sylibr 133 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1332 ⊆ wss 3076 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-in 3082 df-ss 3089 |
This theorem is referenced by: eqsstrrid 3149 inss 3311 difsnss 3674 tpssi 3694 peano5 4520 xpsspw 4659 iotanul 5111 iotass 5113 fun 5303 fun11iun 5396 fvss 5443 fmpt 5578 fliftrel 5701 opabbrex 5823 1stcof 6069 2ndcof 6070 tfrlemibacc 6231 tfrlemibfn 6233 tfr1onlemssrecs 6244 tfr1onlembacc 6247 tfr1onlembfn 6249 tfrcllemssrecs 6257 tfrcllembacc 6260 tfrcllembfn 6262 caucvgprlemladdrl 7510 peano5nnnn 7724 peano5nni 8747 un0addcl 9034 un0mulcl 9035 strleund 12086 cnptopco 12430 cnconst2 12441 xmetresbl 12648 blsscls2 12701 bj-omtrans 13325 |
Copyright terms: Public domain | W3C validator |