Theorem ss2in 4200

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4197	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4198	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3961	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 397   ∩ cin 3913   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3407  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  disjxiun  5106  f1un  6808  undomOLD  9010  strleun  17037  dprdss  19816  dprd2da  19829  ablfac1b  19857  tgcl  22342  innei  22499  hausnei2  22727  bwth  22784  fbssfi  23211  fbunfip  23243  fgcl  23252  blin2  23805  vtxdun  28478  vtxdginducedm1  28540  5oai  30652  mayetes3i  30720  mdsl0  31301  neibastop1  34884  ismblfin  36169  heibor1lem  36318  pl42lem2N  38493  pl42lem3N  38494  ntrk2imkb  42401  ssin0  43355  iscnrm3llem2  47073