Theorem ssinss1 4205

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

Syntax hints:   → wi 4   ∩ cin 3910   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918  df-ss 3928

This theorem is referenced by:  ssinss1d  4206  inss  4207  inindif  4334  fipwuni  9353  ssfin4  10239  insubm  18727  distop  22915  fctop  22924  cctop  22926  ntrin  22981  innei  23045  lly1stc  23416  txcnp  23540  isfild  23778  utoptop  24155  restmetu  24491  lecmi  31581  mdslj2i  32299  mdslmd1lem1  32304  mdslmd1lem2  32305  elpwincl1  32504  pnfneige0  33934  inelcarsg  34295  ballotlemfrc  34511  bnj1177  34989  bnj1311  35007  cldbnd  36307  neiin  36313  ontgval  36412  mblfinlem4  37647  pmodlem1  39833  pmodlem2  39834  pmod1i  39835  pmod2iN  39836  pmodl42N  39838  dochdmj1  41377  redvmptabs  42341  ssficl  43551  ntrclskb  44051  ntrclsk13  44053  ntrneik3  44078  ntrneik13  44080  sswfaxreg  44970  icccncfext  45878  fourierdlem48  46145  fourierdlem49  46146  fourierdlem113  46210  caragendifcl  46505  omelesplit  46509  carageniuncllem2  46513  carageniuncl  46514