Theorem ssinss1 4193

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

Syntax hints:   → wi 4   ∩ cin 3896   ⊆ wss 3897

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904  df-ss 3914

This theorem is referenced by:  ssinss1d  4194  inss  4195  inindif  4322  fipwuni  9310  ssfin4  10201  insubm  18726  distop  22910  fctop  22919  cctop  22921  ntrin  22976  innei  23040  lly1stc  23411  txcnp  23535  isfild  23773  utoptop  24149  restmetu  24485  lecmi  31582  mdslj2i  32300  mdslmd1lem1  32305  mdslmd1lem2  32306  elpwincl1  32505  pnfneige0  33964  inelcarsg  34324  ballotlemfrc  34540  bnj1177  35018  bnj1311  35036  cldbnd  36370  neiin  36376  ontgval  36475  mblfinlem4  37710  pmodlem1  39955  pmodlem2  39956  pmod1i  39957  pmod2iN  39958  pmodl42N  39960  dochdmj1  41499  redvmptabs  42463  ssficl  43672  ntrclskb  44172  ntrclsk13  44174  ntrneik3  44199  ntrneik13  44201  sswfaxreg  45090  icccncfext  45995  fourierdlem48  46262  fourierdlem49  46263  fourierdlem113  46327  caragendifcl  46622  omelesplit  46626  carageniuncllem2  46630  carageniuncl  46631