Theorem ssinss1 4202

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

Syntax hints:   → wi 4   ∩ cin 3912   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  inss  4203  wfrlem4OLD  8263  wfrlem5OLD  8264  fipwuni  9371  ssfin4  10255  insubm  18643  distop  22382  fctop  22391  cctop  22393  ntrin  22449  innei  22513  lly1stc  22884  txcnp  23008  isfild  23246  utoptop  23623  restmetu  23963  lecmi  30607  mdslj2i  31325  mdslmd1lem1  31330  mdslmd1lem2  31331  elpwincl1  31517  pnfneige0  32621  inelcarsg  33000  ballotlemfrc  33215  bnj1177  33707  bnj1311  33725  cldbnd  34874  neiin  34880  ontgval  34979  mblfinlem4  36191  pmodlem1  38382  pmodlem2  38383  pmod1i  38384  pmod2iN  38385  pmodl42N  38387  dochdmj1  39926  ssficl  41963  ntrclskb  42463  ntrclsk13  42465  ntrneik3  42490  ntrneik13  42492  ssinss1d  43378  icccncfext  44248  fourierdlem48  44515  fourierdlem49  44516  fourierdlem113  44580  caragendifcl  44875  omelesplit  44879  carageniuncllem2  44883  carageniuncl  44884