Theorem ssinss1 4209

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 4200	. 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴
2		sstr2 3953	. 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ∩ cin 3913   ⊆ wss 3914

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  ssinss1d  4210  inss  4211  inindif  4338  fipwuni  9377  ssfin4  10263  insubm  18745  distop  22882  fctop  22891  cctop  22893  ntrin  22948  innei  23012  lly1stc  23383  txcnp  23507  isfild  23745  utoptop  24122  restmetu  24458  lecmi  31531  mdslj2i  32249  mdslmd1lem1  32254  mdslmd1lem2  32255  elpwincl1  32454  pnfneige0  33941  inelcarsg  34302  ballotlemfrc  34518  bnj1177  34996  bnj1311  35014  cldbnd  36314  neiin  36320  ontgval  36419  mblfinlem4  37654  pmodlem1  39840  pmodlem2  39841  pmod1i  39842  pmod2iN  39843  pmodl42N  39845  dochdmj1  41384  redvmptabs  42348  ssficl  43558  ntrclskb  44058  ntrclsk13  44060  ntrneik3  44085  ntrneik13  44087  sswfaxreg  44977  icccncfext  45885  fourierdlem48  46152  fourierdlem49  46153  fourierdlem113  46217  caragendifcl  46512  omelesplit  46516  carageniuncllem2  46520  carageniuncl  46521