Theorem ssinss1 4237

Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.)

Assertion

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

Proof of Theorem ssinss1

Step	Hyp	Ref	Expression
1		inss1 4228	. 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
2		sstr2 3989	. 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶))
3	1, 2	ax-mp 5	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-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  inss  4238  wfrlem4OLD  8318  wfrlem5OLD  8319  fipwuni  9427  ssfin4  10311  insubm  18741  distop  22818  fctop  22827  cctop  22829  ntrin  22885  innei  22949  lly1stc  23320  txcnp  23444  isfild  23682  utoptop  24059  restmetu  24399  lecmi  31289  mdslj2i  32007  mdslmd1lem1  32012  mdslmd1lem2  32013  elpwincl1  32197  pnfneige0  33396  inelcarsg  33775  ballotlemfrc  33990  bnj1177  34482  bnj1311  34500  cldbnd  35677  neiin  35683  ontgval  35782  mblfinlem4  36994  pmodlem1  39183  pmodlem2  39184  pmod1i  39185  pmod2iN  39186  pmodl42N  39188  dochdmj1  40727  ssficl  42785  ntrclskb  43285  ntrclsk13  43287  ntrneik3  43312  ntrneik13  43314  ssinss1d  44199  icccncfext  45064  fourierdlem48  45331  fourierdlem49  45332  fourierdlem113  45396  caragendifcl  45691  omelesplit  45695  carageniuncllem2  45699  carageniuncl  45700