Theorem ssinss1 4214

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

Syntax hints:   → wi 4   ∩ cin 3935   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  inss  4215  wfrlem4  7958  wfrlem5  7959  fipwuni  8890  ssfin4  9732  insubm  17983  distop  21603  fctop  21612  cctop  21614  ntrin  21669  innei  21733  lly1stc  22104  txcnp  22228  isfild  22466  utoptop  22843  restmetu  23180  lecmi  29379  mdslj2i  30097  mdslmd1lem1  30102  mdslmd1lem2  30103  elpwincl1  30286  pnfneige0  31194  inelcarsg  31569  ballotlemfrc  31784  bnj1177  32278  bnj1311  32296  cldbnd  33674  neiin  33680  ontgval  33779  mblfinlem4  34947  pmodlem1  36997  pmodlem2  36998  pmod1i  36999  pmod2iN  37000  pmodl42N  37002  dochdmj1  38541  ssficl  39948  ntrclskb  40439  ntrclsk13  40441  ntrneik3  40466  ntrneik13  40468  ssinss1d  41330  icccncfext  42190  fourierdlem48  42459  fourierdlem49  42460  fourierdlem113  42524  caragendifcl  42816  omelesplit  42820  carageniuncllem2  42824  carageniuncl  42825