![]() |
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 3988 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2an 595 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3473 df-in 3954 df-ss 3964 |
This theorem is referenced by: sylan9ssr 3994 psstr 4102 unss12 4182 ss2in 4237 ssdisj 4460 relrelss 6277 funssxp 6752 axdc3lem 10474 tskuni 10807 rtrclreclem4 15041 tsmsxp 24072 shslubi 31208 chlej12i 31298 insiga 33756 fnetr 35835 pcl0bN 39396 brtrclfv2 43157 |
Copyright terms: Public domain | W3C validator |