![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sseqtrrdi | GIF version |
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.) |
Ref | Expression |
---|---|
sseqtrrdi.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
sseqtrrdi.2 | ⊢ 𝐶 = 𝐵 |
Ref | Expression |
---|---|
sseqtrrdi | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseqtrrdi.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | sseqtrrdi.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
3 | 2 | eqcomi 2197 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | sseqtrdi 3227 | 1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 ⊆ wss 3153 |
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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2175 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2180 df-cleq 2186 df-clel 2189 df-in 3159 df-ss 3166 |
This theorem is referenced by: iunpw 4511 iotanul 5230 iotass 5232 tfrlem9 6372 tfrlemibfn 6381 tfrlemiubacc 6383 tfrlemi14d 6386 tfr1onlemssrecs 6392 tfr1onlemres 6402 tfrcllemres 6415 exmidfodomrlemr 7262 exmidfodomrlemrALT 7263 uznnssnn 9642 shftfvalg 10962 shftfval 10965 clim2prod 11682 reldvdsrsrg 13588 dvdsrvald 13589 dvdsrex 13594 eltopss 14177 difopn 14276 tgrest 14337 txuni2 14424 tgioo 14714 |
Copyright terms: Public domain | W3C validator |