Theorem ssinss1 4195

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 4186	. 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  4196  inss  4197  inindif  4324  fipwuni  9316  ssfin4  10207  insubm  18732  distop  22916  fctop  22925  cctop  22927  ntrin  22982  innei  23046  lly1stc  23417  txcnp  23541  isfild  23779  utoptop  24155  restmetu  24491  lecmi  31589  mdslj2i  32307  mdslmd1lem1  32312  mdslmd1lem2  32313  elpwincl1  32512  pnfneige0  33971  inelcarsg  34331  ballotlemfrc  34547  bnj1177  35025  bnj1311  35043  cldbnd  36377  neiin  36383  ontgval  36482  mblfinlem4  37706  pmodlem1  39951  pmodlem2  39952  pmod1i  39953  pmod2iN  39954  pmodl42N  39956  dochdmj1  41495  redvmptabs  42459  ssficl  43667  ntrclskb  44167  ntrclsk13  44169  ntrneik3  44194  ntrneik13  44196  sswfaxreg  45085  icccncfext  45990  fourierdlem48  46257  fourierdlem49  46258  fourierdlem113  46322  caragendifcl  46617  omelesplit  46621  carageniuncllem2  46625  carageniuncl  46626