Theorem ssinss1 4200

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 4191	. 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 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 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  ssinss1d  4201  inss  4202  inindif  4329  fipwuni  9341  ssfin4  10232  insubm  18755  distop  22951  fctop  22960  cctop  22962  ntrin  23017  innei  23081  lly1stc  23452  txcnp  23576  isfild  23814  utoptop  24190  restmetu  24526  lecmi  31690  mdslj2i  32408  mdslmd1lem1  32413  mdslmd1lem2  32414  elpwincl1  32612  pnfneige0  34129  inelcarsg  34489  ballotlemfrc  34705  bnj1177  35182  bnj1311  35200  cldbnd  36542  neiin  36548  ontgval  36647  mblfinlem4  37911  pmodlem1  40222  pmodlem2  40223  pmod1i  40224  pmod2iN  40225  pmodl42N  40227  dochdmj1  41766  redvmptabs  42730  ssficl  43925  ntrclskb  44425  ntrclsk13  44427  ntrneik3  44452  ntrneik13  44454  sswfaxreg  45343  icccncfext  46245  fourierdlem48  46512  fourierdlem49  46513  fourierdlem113  46577  caragendifcl  46872  omelesplit  46876  carageniuncllem2  46880  carageniuncl  46881