![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9ss | Structured version Visualization version GIF version |
Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Ref | Expression |
---|---|
sylan9ss.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
sylan9ss.2 | ⊢ (𝜓 → 𝐵 ⊆ 𝐶) |
Ref | Expression |
---|---|
sylan9ss | ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9ss.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | sylan9ss.2 | . 2 ⊢ (𝜓 → 𝐵 ⊆ 𝐶) | |
3 | sstr 4003 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2an 596 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ss 3979 |
This theorem is referenced by: sylan9ssr 4009 psstr 4116 unss12 4197 ss2in 4252 ssdisj 4465 relrelss 6294 funssxp 6764 axdc3lem 10487 tskuni 10820 rtrclreclem4 15096 tsmsxp 24178 shslubi 31413 chlej12i 31503 insiga 34117 fnetr 36333 pcl0bN 39905 brtrclfv2 43716 |
Copyright terms: Public domain | W3C validator |