![]() |
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 3990 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2an 595 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3955 df-ss 3965 |
This theorem is referenced by: sylan9ssr 3996 psstr 4104 unss12 4182 ss2in 4236 ssdisj 4459 relrelss 6272 funssxp 6746 axdc3lem 10449 tskuni 10782 rtrclreclem4 15013 tsmsxp 23880 shslubi 30906 chlej12i 30996 insiga 33434 fnetr 35540 pcl0bN 39098 brtrclfv2 42781 |
Copyright terms: Public domain | W3C validator |