Theorem ssinss1 3803

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

Syntax hints:   → wi 4   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  inss  3804  wfrlem4  7305  wfrlem5  7306  fipwuni  8215  ssfin4  9015  distop  20610  fctop  20618  cctop  20620  ntrin  20675  innei  20739  lly1stc  21109  txcnp  21233  isfild  21472  utoptop  21848  restmetu  22185  lecmi  27845  mdslj2i  28563  mdslmd1lem1  28568  mdslmd1lem2  28569  elpwincl1  28741  pnfneige0  29325  inelcarsg  29700  ballotlemfrc  29915  bnj1177  30328  bnj1311  30346  frrlem4  31027  frrlem5  31028  cldbnd  31491  neiin  31497  ontgval  31600  mblfinlem4  32619  pmodlem1  34150  pmodlem2  34151  pmod1i  34152  pmod2iN  34153  pmodl42N  34155  dochdmj1  35697  ssficl  36893  ntrclskb  37387  ntrclsk13  37389  ntrneik3  37414  ntrneik13  37416  ssinss1d  38239  icccncfext  38773  fourierdlem48  39047  fourierdlem49  39048  fourierdlem113  39112  caragendifcl  39404  omelesplit  39408  carageniuncllem2  39412  carageniuncl  39413