Theorem ssinss1 4216

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

Syntax hints:   → wi 4   ∩ cin 3937   ⊆ wss 3938

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954

This theorem is referenced by:  inss  4217  wfrlem4  7960  wfrlem5  7961  fipwuni  8892  ssfin4  9734  insubm  17985  distop  21605  fctop  21614  cctop  21616  ntrin  21671  innei  21735  lly1stc  22106  txcnp  22230  isfild  22468  utoptop  22845  restmetu  23182  lecmi  29381  mdslj2i  30099  mdslmd1lem1  30104  mdslmd1lem2  30105  elpwincl1  30288  pnfneige0  31196  inelcarsg  31571  ballotlemfrc  31786  bnj1177  32280  bnj1311  32298  cldbnd  33676  neiin  33682  ontgval  33781  mblfinlem4  34934  pmodlem1  36984  pmodlem2  36985  pmod1i  36986  pmod2iN  36987  pmodl42N  36989  dochdmj1  38528  ssficl  39935  ntrclskb  40426  ntrclsk13  40428  ntrneik3  40453  ntrneik13  40455  ssinss1d  41317  icccncfext  42177  fourierdlem48  42446  fourierdlem49  42447  fourierdlem113  42511  caragendifcl  42803  omelesplit  42807  carageniuncllem2  42811  carageniuncl  42812