Theorem ss2in 3802

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 3800	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 3801	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3581	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 383   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  disjxiun  4579  disjxiunOLD  4580  undom  7933  strlemor1  15796  strleun  15799  dprdss  18251  dprd2da  18264  ablfac1b  18292  tgcl  20584  innei  20739  hausnei2  20967  bwth  21023  fbssfi  21451  fbunfip  21483  fgcl  21492  blin2  22044  vdgrun  26428  vdgrfiun  26429  5oai  27904  mayetes3i  27972  mdsl0  28553  neibastop1  31524  ismblfin  32620  heibor1lem  32778  pl42lem2N  34284  pl42lem3N  34285  ntrk2imkb  37355  ssin0  38248  vtxdun  40696