Theorem ss2in 4151

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4148	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4149	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3914	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

Syntax hints:   → wi 4   ∧ wa 399   ∩ cin 3865   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  disjxiun  5050  undom  8733  strleun  16710  dprdss  19416  dprd2da  19429  ablfac1b  19457  tgcl  21866  innei  22022  hausnei2  22250  bwth  22307  fbssfi  22734  fbunfip  22766  fgcl  22775  blin2  23327  vtxdun  27569  vtxdginducedm1  27631  5oai  29742  mayetes3i  29810  mdsl0  30391  neibastop1  34285  ismblfin  35555  heibor1lem  35704  pl42lem2N  37731  pl42lem3N  37732  ntrk2imkb  41324  ssin0  42276  iscnrm3llem2  45917