Theorem ssinss1 4186

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

Syntax hints:   → wi 4   ∩ cin 3888   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  ssinss1d  4187  inss  4188  inindif  4315  fipwuni  9339  ssfin4  10232  insubm  18786  distop  22960  fctop  22969  cctop  22971  ntrin  23026  innei  23090  lly1stc  23461  txcnp  23585  isfild  23823  utoptop  24199  restmetu  24535  lecmi  31673  mdslj2i  32391  mdslmd1lem1  32396  mdslmd1lem2  32397  elpwincl1  32595  pnfneige0  34095  inelcarsg  34455  ballotlemfrc  34671  bnj1177  35148  bnj1311  35166  cldbnd  36508  neiin  36514  ontgval  36613  mblfinlem4  37981  pmodlem1  40292  pmodlem2  40293  pmod1i  40294  pmod2iN  40295  pmodl42N  40297  dochdmj1  41836  redvmptabs  42792  ssficl  43996  ntrclskb  44496  ntrclsk13  44498  ntrneik3  44523  ntrneik13  44525  sswfaxreg  45414  icccncfext  46315  fourierdlem48  46582  fourierdlem49  46583  fourierdlem113  46647  caragendifcl  46942  omelesplit  46946  carageniuncllem2  46950  carageniuncl  46951