Theorem ss2in 4199

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

Assertion

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

Proof of Theorem ss2in

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-in 3914  df-ss 3924

This theorem is referenced by:  disjxiun  5101  f1un  6831  strleun  17205  dprdss  20089  dprd2da  20102  ablfac1b  20130  tgcl  23083  innei  23239  hausnei2  23467  bwth  23524  fbssfi  23951  fbunfip  23983  fgcl  23992  blin2  24543  vtxdun  29736  vtxdginducedm1  29798  5oai  31918  mayetes3i  31986  mdsl0  32567  neibastop1  36727  ismblfin  38167  heibor1lem  38315  pl42lem2N  40611  pl42lem3N  40612  ntrk2imkb  44620  ssin0  45634  iscnrm3llem2  49580