Theorem ss2in 4253

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4250	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4251	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 4009	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   ∩ cin 3962   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980

This theorem is referenced by:  disjxiun  5145  f1un  6869  undomOLD  9099  strleun  17191  dprdss  20064  dprd2da  20077  ablfac1b  20105  tgcl  22992  innei  23149  hausnei2  23377  bwth  23434  fbssfi  23861  fbunfip  23893  fgcl  23902  blin2  24455  vtxdun  29514  vtxdginducedm1  29576  5oai  31690  mayetes3i  31758  mdsl0  32339  neibastop1  36342  ismblfin  37648  heibor1lem  37796  pl42lem2N  39963  pl42lem3N  39964  ntrk2imkb  44027  ssin0  44995  iscnrm3llem2  48747