Theorem ssinss1 4267

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

Syntax hints:   → wi 4   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  inss  4268  wfrlem4OLD  8368  wfrlem5OLD  8369  fipwuni  9495  ssfin4  10379  insubm  18853  distop  23023  fctop  23032  cctop  23034  ntrin  23090  innei  23154  lly1stc  23525  txcnp  23649  isfild  23887  utoptop  24264  restmetu  24604  lecmi  31634  mdslj2i  32352  mdslmd1lem1  32357  mdslmd1lem2  32358  elpwincl1  32555  pnfneige0  33897  inelcarsg  34276  ballotlemfrc  34491  bnj1177  34982  bnj1311  35000  cldbnd  36292  neiin  36298  ontgval  36397  mblfinlem4  37620  pmodlem1  39803  pmodlem2  39804  pmod1i  39805  pmod2iN  39806  pmodl42N  39808  dochdmj1  41347  ssficl  43531  ntrclskb  44031  ntrclsk13  44033  ntrneik3  44058  ntrneik13  44060  ssinss1d  44950  icccncfext  45808  fourierdlem48  46075  fourierdlem49  46076  fourierdlem113  46140  caragendifcl  46435  omelesplit  46439  carageniuncllem2  46443  carageniuncl  46444