Theorem ssinss1 4174

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

Syntax hints:   → wi 4   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890  df-ss 3900

This theorem is referenced by:  ssinss1d  4175  inss  4176  inindif  4303  fipwuni  9329  ssfin4  10223  insubm  18777  distop  22978  fctop  22987  cctop  22989  ntrin  23044  innei  23108  lly1stc  23479  txcnp  23603  isfild  23841  utoptop  24217  restmetu  24553  lecmi  31691  mdslj2i  32409  mdslmd1lem1  32414  mdslmd1lem2  32415  elpwincl1  32613  pnfneige0  34135  inelcarsg  34495  ballotlemfrc  34711  bnj1177  35188  bnj1311  35206  cldbnd  36554  neiin  36560  ontgval  36659  mblfinlem4  38027  pmodlem1  40338  pmodlem2  40339  pmod1i  40340  pmod2iN  40341  pmodl42N  40343  dochdmj1  41882  redvmptabs  42837  ssficl  44013  ntrclskb  44513  ntrclsk13  44515  ntrneik3  44540  ntrneik13  44542  sswfaxreg  45431  icccncfext  46330  fourierdlem48  46597  fourierdlem49  46598  fourierdlem113  46662  caragendifcl  46957  omelesplit  46961  carageniuncllem2  46965  carageniuncl  46966