Theorem ssinss1 4152

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

Syntax hints:   → wi 4   ∩ cin 3865   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  inss  4153  wfrlem4  8058  wfrlem5  8059  fipwuni  9042  ssfin4  9924  insubm  18245  distop  21892  fctop  21901  cctop  21903  ntrin  21958  innei  22022  lly1stc  22393  txcnp  22517  isfild  22755  utoptop  23132  restmetu  23468  lecmi  29683  mdslj2i  30401  mdslmd1lem1  30406  mdslmd1lem2  30407  elpwincl1  30593  pnfneige0  31615  inelcarsg  31990  ballotlemfrc  32205  bnj1177  32699  bnj1311  32717  cldbnd  34252  neiin  34258  ontgval  34357  mblfinlem4  35554  pmodlem1  37597  pmodlem2  37598  pmod1i  37599  pmod2iN  37600  pmodl42N  37602  dochdmj1  39141  ssficl  40852  ntrclskb  41356  ntrclsk13  41358  ntrneik3  41383  ntrneik13  41385  ssinss1d  42269  icccncfext  43103  fourierdlem48  43370  fourierdlem49  43371  fourierdlem113  43435  caragendifcl  43727  omelesplit  43731  carageniuncllem2  43735  carageniuncl  43736