![]() |
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 3181 | . 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶) |
4 | 1, 3 | sylibr 134 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 ⊆ wss 3129 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-11 1506 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-in 3135 df-ss 3142 |
This theorem is referenced by: eqsstrrid 3202 inss 3365 difsnss 3738 tpssi 3759 peano5 4596 xpsspw 4737 iotanul 5192 iotass 5194 fun 5387 fun11iun 5481 fvss 5528 fmpt 5665 fliftrel 5790 opabbrex 5916 1stcof 6161 2ndcof 6162 tfrlemibacc 6324 tfrlemibfn 6326 tfr1onlemssrecs 6337 tfr1onlembacc 6340 tfr1onlembfn 6342 tfrcllemssrecs 6350 tfrcllembacc 6353 tfrcllembfn 6355 caucvgprlemladdrl 7674 peano5nnnn 7888 peano5nni 8918 un0addcl 9205 un0mulcl 9206 strleund 12554 mgmidsssn0 12735 cnptopco 13593 cnconst2 13604 xmetresbl 13811 blsscls2 13864 bj-omtrans 14568 |
Copyright terms: Public domain | W3C validator |