Theorem ss2in 4198

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4195	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4196	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3951	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 400   ∩ cin 3905   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-in 3913  df-ss 3923

This theorem is referenced by:  disjxiun  5107  f1un  6843  strleun  17218  dprdss  20102  dprd2da  20115  ablfac1b  20143  tgcl  23107  innei  23263  hausnei2  23491  bwth  23548  fbssfi  23975  fbunfip  24007  fgcl  24016  blin2  24567  vtxdun  29812  vtxdginducedm1  29874  5oai  31994  mayetes3i  32062  mdsl0  32643  neibastop1  36851  ismblfin  38293  heibor1lem  38441  pl42lem2N  40735  pl42lem3N  40736  ntrk2imkb  44746  ssin0  45758  iscnrm3llem2  49711