Theorem ss2in 4141

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

Assertion

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

Proof of Theorem ss2in

Step	Hyp	Ref	Expression
1		ssrin 4138	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		sslin 4139	. 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))
3	1, 2	sylan9ss 3921	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  disjxiun  5099  f1un  6846  strleun  17341  dprdss  20251  dprd2da  20264  ablfac1b  20292  tgcl  23293  innei  23449  hausnei2  23677  bwth  23734  fbssfi  24162  fbunfip  24194  fgcl  24203  blin2  24754  vtxdun  30068  vtxdginducedm1  30130  5oai  32269  mayetes3i  32337  mdsl0  32918  neibastop1  37240  ismblfin  38673  heibor1lem  38837  pl42lem2N  41131  pl42lem3N  41132  ntrk2imkb  45131  ssin0  46166  iscnrm3llem2  50158