Theorem ssinss1 4198

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

Syntax hints:   → wi 4   ∩ cin 3900   ⊆ wss 3901

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  ssinss1d  4199  inss  4200  inindif  4327  fipwuni  9329  ssfin4  10220  insubm  18743  distop  22939  fctop  22948  cctop  22950  ntrin  23005  innei  23069  lly1stc  23440  txcnp  23564  isfild  23802  utoptop  24178  restmetu  24514  lecmi  31677  mdslj2i  32395  mdslmd1lem1  32400  mdslmd1lem2  32401  elpwincl1  32600  pnfneige0  34108  inelcarsg  34468  ballotlemfrc  34684  bnj1177  35162  bnj1311  35180  cldbnd  36520  neiin  36526  ontgval  36625  mblfinlem4  37861  pmodlem1  40116  pmodlem2  40117  pmod1i  40118  pmod2iN  40119  pmodl42N  40121  dochdmj1  41660  redvmptabs  42625  ssficl  43820  ntrclskb  44320  ntrclsk13  44322  ntrneik3  44347  ntrneik13  44349  sswfaxreg  45238  icccncfext  46141  fourierdlem48  46408  fourierdlem49  46409  fourierdlem113  46473  caragendifcl  46768  omelesplit  46772  carageniuncllem2  46776  carageniuncl  46777