Theorem ss2in 4196

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4193	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4194	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3945	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3898   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-in 3906  df-ss 3916

This theorem is referenced by:  disjxiun  5092  f1un  6791  strleun  17078  dprdss  19953  dprd2da  19966  ablfac1b  19994  tgcl  22894  innei  23050  hausnei2  23278  bwth  23335  fbssfi  23762  fbunfip  23794  fgcl  23803  blin2  24354  vtxdun  29471  vtxdginducedm1  29533  5oai  31652  mayetes3i  31720  mdsl0  32301  neibastop1  36414  ismblfin  37711  heibor1lem  37859  pl42lem2N  40089  pl42lem3N  40090  ntrk2imkb  44144  ssin0  45166  iscnrm3llem2  49064