Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ss2in | Structured version Visualization version GIF version |
Description: Intersection of subclasses. (Contributed by NM, 5-May-2000.) |
Ref | Expression |
---|---|
ss2in | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrin 3838 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | sslin 3839 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | |
3 | 1, 2 | sylan9ss 3616 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∩ cin 3573 ⊆ wss 3574 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 |
This theorem is referenced by: disjxiun 4649 disjxiunOLD 4650 undom 8048 strlemor1OLD 15969 strleun 15972 dprdss 18428 dprd2da 18441 ablfac1b 18469 tgcl 20773 innei 20929 hausnei2 21157 bwth 21213 fbssfi 21641 fbunfip 21673 fgcl 21682 blin2 22234 vtxdun 26377 vtxdginducedm1 26439 5oai 28520 mayetes3i 28588 mdsl0 29169 neibastop1 32354 ismblfin 33450 heibor1lem 33608 pl42lem2N 35266 pl42lem3N 35267 ntrk2imkb 38335 ssin0 39223 |
Copyright terms: Public domain | W3C validator |