| 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 3992 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | |
| 4 | 1, 2, 3 | syl2an 596 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ss 3968 |
| This theorem is referenced by: sylan9ssr 3998 psstr 4107 unss12 4188 ss2in 4245 ssdisj 4460 relrelss 6293 funssxp 6764 axdc3lem 10490 tskuni 10823 rtrclreclem4 15100 tsmsxp 24163 shslubi 31404 chlej12i 31494 insiga 34138 fnetr 36352 pcl0bN 39925 brtrclfv2 43740 |
| Copyright terms: Public domain | W3C validator |