Theorem ssinss1 4171

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

Syntax hints:   → wi 4   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  inss  4172  wfrlem4OLD  8143  wfrlem5OLD  8144  fipwuni  9185  ssfin4  10066  insubm  18457  distop  22145  fctop  22154  cctop  22156  ntrin  22212  innei  22276  lly1stc  22647  txcnp  22771  isfild  23009  utoptop  23386  restmetu  23726  lecmi  29964  mdslj2i  30682  mdslmd1lem1  30687  mdslmd1lem2  30688  elpwincl1  30874  pnfneige0  31901  inelcarsg  32278  ballotlemfrc  32493  bnj1177  32986  bnj1311  33004  cldbnd  34515  neiin  34521  ontgval  34620  mblfinlem4  35817  pmodlem1  37860  pmodlem2  37861  pmod1i  37862  pmod2iN  37863  pmodl42N  37865  dochdmj1  39404  ssficl  41176  ntrclskb  41679  ntrclsk13  41681  ntrneik3  41706  ntrneik13  41708  ssinss1d  42596  icccncfext  43428  fourierdlem48  43695  fourierdlem49  43696  fourierdlem113  43760  caragendifcl  44052  omelesplit  44056  carageniuncllem2  44060  carageniuncl  44061