Theorem sslin 4234

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

Syntax hints:   → wi 4   ∩ cin 3947   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  ss2in  4236  inxpssres  5693  ssres2  6009  predrelss  6338  sbthlem7  9095  kmlem5  10155  canthnum  10650  ioodisj  13466  hashun3  14351  dprdres  19946  dprd2da  19960  dmdprdsplit2lem  19963  srhmsubc  20572  rhmsubclem3  20579  fldc  20631  fldhmsubc  20632  cnprest  23113  isnrm3  23183  regsep2  23200  llycmpkgen2  23374  kqdisj  23556  regr1lem  23563  fclsbas  23845  fclscf  23849  flimfnfcls  23852  isfcf  23858  metdstri  24687  nulmbl2  25385  uniioombllem4  25435  volsup2  25454  volcn  25455  itg1climres  25564  limcresi  25734  limciun  25743  rlimcnp2  26812  rplogsum  27373  chssoc  31182  cmbr4i  31287  5oai  31347  3oalem6  31353  mdslmd4i  32019  atcvat4i  32083  imadifxp  32265  swrdrndisj  32554  crefss  33293  pnfneige0  33395  cldbnd  35675  neibastop1  35708  neibastop2  35710  onint1  35798  oninhaus  35799  bj-idres  36505  cntotbnd  37128  polcon3N  39252  osumcllem4N  39294  lcfrlem2  40878  mapfzcons1  41918  coeq0i  41954  eldioph4b  42012  icccncfext  45062  rhmsubcALTVlem4  47121  srhmsubcALTV  47162  fldcALTV  47169  fldhmsubcALTV  47170  ssdisjdr  47655  sepnsepolem2  47717