![]() |
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 4032 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | sslin 4033 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | |
3 | 1, 2 | sylan9ss 3810 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 ∩ cin 3767 ⊆ wss 3768 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2776 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-v 3386 df-in 3775 df-ss 3782 |
This theorem is referenced by: disjxiun 4839 undom 8289 strleun 16290 dprdss 18741 dprd2da 18754 ablfac1b 18782 tgcl 21099 innei 21255 hausnei2 21483 bwth 21539 fbssfi 21966 fbunfip 21998 fgcl 22007 blin2 22559 vtxdun 26724 vtxdginducedm1 26786 5oai 29038 mayetes3i 29106 mdsl0 29687 neibastop1 32859 ismblfin 33932 heibor1lem 34088 pl42lem2N 35994 pl42lem3N 35995 ntrk2imkb 39106 ssin0 39971 |
Copyright terms: Public domain | W3C validator |