Theorem sslin 4210

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 4209	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		incom 4177	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4177	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3sstr4g 4011	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   ∩ cin 3934   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-in 3942  df-ss 3951

This theorem is referenced by:  ss2in  4212  inxpssres  5566  ssres2  5875  sbthlem7  8627  kmlem5  9574  canthnum  10065  ioodisj  12862  hashun3  13739  dprdres  19144  dprd2da  19158  dmdprdsplit2lem  19161  cnprest  21891  isnrm3  21961  regsep2  21978  llycmpkgen2  22152  kqdisj  22334  regr1lem  22341  fclsbas  22623  fclscf  22627  flimfnfcls  22630  isfcf  22636  metdstri  23453  nulmbl2  24131  uniioombllem4  24181  volsup2  24200  volcn  24201  itg1climres  24309  limcresi  24477  limciun  24486  rlimcnp2  25538  rplogsum  26097  chssoc  29267  cmbr4i  29372  5oai  29432  3oalem6  29438  mdslmd4i  30104  atcvat4i  30168  imadifxp  30345  swrdrndisj  30626  crefss  31108  pnfneige0  31189  cldbnd  33669  neibastop1  33702  neibastop2  33704  onint1  33792  oninhaus  33793  bj-idres  34446  cntotbnd  35068  polcon3N  37047  osumcllem4N  37089  lcfrlem2  38673  mapfzcons1  39307  coeq0i  39343  eldioph4b  39401  icccncfext  42163  srhmsubc  44341  fldc  44348  fldhmsubc  44349  rhmsubclem3  44353  srhmsubcALTV  44359  fldcALTV  44366  fldhmsubcALTV  44367  rhmsubcALTVlem4  44372