Theorem ssinss1 4254

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

Syntax hints:   → wi 4   ∩ cin 3962   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-in 3970  df-ss 3980

This theorem is referenced by:  inss  4255  inindif  4381  wfrlem4OLD  8351  wfrlem5OLD  8352  fipwuni  9464  ssfin4  10348  insubm  18844  distop  23018  fctop  23027  cctop  23029  ntrin  23085  innei  23149  lly1stc  23520  txcnp  23644  isfild  23882  utoptop  24259  restmetu  24599  lecmi  31631  mdslj2i  32349  mdslmd1lem1  32354  mdslmd1lem2  32355  elpwincl1  32553  pnfneige0  33912  inelcarsg  34293  ballotlemfrc  34508  bnj1177  34999  bnj1311  35017  cldbnd  36309  neiin  36315  ontgval  36414  mblfinlem4  37647  pmodlem1  39829  pmodlem2  39830  pmod1i  39831  pmod2iN  39832  pmodl42N  39834  dochdmj1  41373  redvmptabs  42369  ssficl  43559  ntrclskb  44059  ntrclsk13  44061  ntrneik3  44086  ntrneik13  44088  ssinss1d  44988  icccncfext  45843  fourierdlem48  46110  fourierdlem49  46111  fourierdlem113  46175  caragendifcl  46470  omelesplit  46474  carageniuncllem2  46478  carageniuncl  46479