Theorem ssinss1 4197

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

Syntax hints:   → wi 4   ∩ cin 3902   ⊆ wss 3903

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 3438  df-in 3910  df-ss 3920

This theorem is referenced by:  ssinss1d  4198  inss  4199  inindif  4326  fipwuni  9316  ssfin4  10204  insubm  18692  distop  22880  fctop  22889  cctop  22891  ntrin  22946  innei  23010  lly1stc  23381  txcnp  23505  isfild  23743  utoptop  24120  restmetu  24456  lecmi  31546  mdslj2i  32264  mdslmd1lem1  32269  mdslmd1lem2  32270  elpwincl1  32469  pnfneige0  33918  inelcarsg  34279  ballotlemfrc  34495  bnj1177  34973  bnj1311  34991  cldbnd  36304  neiin  36310  ontgval  36409  mblfinlem4  37644  pmodlem1  39829  pmodlem2  39830  pmod1i  39831  pmod2iN  39832  pmodl42N  39834  dochdmj1  41373  redvmptabs  42337  ssficl  43546  ntrclskb  44046  ntrclsk13  44048  ntrneik3  44073  ntrneik13  44075  sswfaxreg  44965  icccncfext  45872  fourierdlem48  46139  fourierdlem49  46140  fourierdlem113  46204  caragendifcl  46499  omelesplit  46503  carageniuncllem2  46507  carageniuncl  46508