Theorem ss2in 4035

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4032	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4033	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3810	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 385   ∩ cin 3767   ⊆ wss 3768

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-nfc 2929  df-v 3386  df-in 3775  df-ss 3782

This theorem is referenced by:  disjxiun  4839  undom  8289  strleun  16290  dprdss  18741  dprd2da  18754  ablfac1b  18782  tgcl  21099  innei  21255  hausnei2  21483  bwth  21539  fbssfi  21966  fbunfip  21998  fgcl  22007  blin2  22559  vtxdun  26724  vtxdginducedm1  26786  5oai  29038  mayetes3i  29106  mdsl0  29687  neibastop1  32859  ismblfin  33932  heibor1lem  34088  pl42lem2N  35994  pl42lem3N  35995  ntrk2imkb  39106  ssin0  39971