Theorem sslin 4209

Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)

Assertion

Ref	Expression
sslin	⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Proof of Theorem sslin

Step	Hyp	Ref	Expression
1		ssrin 4208	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		incom 4175	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4175	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3sstr4g 4003	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   ∩ cin 3916   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  ss2in  4211  inxpssres  5658  ssres2  5978  predrelss  6313  sbthlem7  9063  kmlem5  10115  canthnum  10609  ioodisj  13450  hashun3  14356  dprdres  19967  dprd2da  19981  dmdprdsplit2lem  19984  srhmsubc  20596  rhmsubclem3  20603  fldc  20700  fldhmsubc  20701  cnprest  23183  isnrm3  23253  regsep2  23270  llycmpkgen2  23444  kqdisj  23626  regr1lem  23633  fclsbas  23915  fclscf  23919  flimfnfcls  23922  isfcf  23928  metdstri  24747  nulmbl2  25444  uniioombllem4  25494  volsup2  25513  volcn  25514  itg1climres  25622  limcresi  25793  limciun  25802  rlimcnp2  26883  rplogsum  27445  chssoc  31432  cmbr4i  31537  5oai  31597  3oalem6  31603  mdslmd4i  32269  atcvat4i  32333  imadifxp  32537  swrdrndisj  32886  1arithufdlem4  33525  crefss  33846  pnfneige0  33948  cldbnd  36321  neibastop1  36354  neibastop2  36356  onint1  36444  oninhaus  36445  bj-idres  37155  cntotbnd  37797  polcon3N  39918  osumcllem4N  39960  lcfrlem2  41544  mapfzcons1  42712  coeq0i  42748  eldioph4b  42806  icccncfext  45892  rhmsubcALTVlem4  48276  srhmsubcALTV  48317  fldcALTV  48324  fldhmsubcALTV  48325  ssdisjdr  48801  sepnsepolem2  48915