Theorem ss2in 4194

Description: Intersection of subclasses. (Contributed by NM, 5-May-2000.)

Assertion

Ref	Expression
ss2in	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4191	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4192	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3947	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-in 3909  df-ss 3919

This theorem is referenced by:  disjxiun  5094  f1un  6821  strleun  17183  dprdss  20061  dprd2da  20074  ablfac1b  20102  tgcl  23016  innei  23172  hausnei2  23400  bwth  23457  fbssfi  23884  fbunfip  23916  fgcl  23925  blin2  24476  vtxdun  29638  vtxdginducedm1  29700  5oai  31820  mayetes3i  31888  mdsl0  32469  neibastop1  36679  ismblfin  38120  heibor1lem  38268  pl42lem2N  40564  pl42lem3N  40565  ntrk2imkb  44573  ssin0  45595  iscnrm3llem2  49531