![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sylan9ssr | Structured version Visualization version GIF version |
Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) |
Ref | Expression |
---|---|
sylan9ssr.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
sylan9ssr.2 | ⊢ (𝜓 → 𝐵 ⊆ 𝐶) |
Ref | Expression |
---|---|
sylan9ssr | ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9ssr.1 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | sylan9ssr.2 | . . 3 ⊢ (𝜓 → 𝐵 ⊆ 𝐶) | |
3 | 1, 2 | sylan9ss 3649 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶) |
4 | 3 | ancoms 468 | 1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-in 3614 df-ss 3621 |
This theorem is referenced by: intssuni2 4534 marypha1 8381 cardinfima 8958 cfflb 9119 ssfin4 9170 acsfn 16367 mrelatlub 17233 efgval 18176 islbs3 19203 kgentopon 21389 txlly 21487 sigaclci 30323 bnj1014 31156 topjoin 32485 filnetlem3 32500 poimirlem16 33555 mblfinlem3 33578 sspwimpALT 39475 sspwimpALT2 39478 setrecsres 42773 |
Copyright terms: Public domain | W3C validator |