Theorem ssinss1 4187

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  ssinss1d  4188  inss  4189  inindif  4316  fipwuni  9333  ssfin4  10226  insubm  18780  distop  22973  fctop  22982  cctop  22984  ntrin  23039  innei  23103  lly1stc  23474  txcnp  23598  isfild  23836  utoptop  24212  restmetu  24548  lecmi  31691  mdslj2i  32409  mdslmd1lem1  32414  mdslmd1lem2  32415  elpwincl1  32613  pnfneige0  34114  inelcarsg  34474  ballotlemfrc  34690  bnj1177  35167  bnj1311  35185  cldbnd  36527  neiin  36533  ontgval  36632  mblfinlem4  37998  pmodlem1  40309  pmodlem2  40310  pmod1i  40311  pmod2iN  40312  pmodl42N  40314  dochdmj1  41853  redvmptabs  42809  ssficl  44017  ntrclskb  44517  ntrclsk13  44519  ntrneik3  44544  ntrneik13  44546  sswfaxreg  45435  icccncfext  46336  fourierdlem48  46603  fourierdlem49  46604  fourierdlem113  46668  caragendifcl  46963  omelesplit  46967  carageniuncllem2  46971  carageniuncl  46972