![]() |
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 3752 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2an 495 | 1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊆ wss 3715 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-in 3722 df-ss 3729 |
This theorem is referenced by: sylan9ssr 3758 psstr 3853 unss12 3928 ss2in 3983 ssdisj 4170 relrelss 5820 funssxp 6222 axdc3lem 9464 tskuni 9797 rtrclreclem4 14000 tsmsxp 22159 shslubi 28553 chlej12i 28643 insiga 30509 fnetr 32652 pcl0bN 35712 brtrclfv2 38521 |
Copyright terms: Public domain | W3C validator |