Theorem ssinss1 4168

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

Syntax hints:   → wi 4   ∩ cin 3882   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  inss  4169  wfrlem4OLD  8114  wfrlem5OLD  8115  fipwuni  9115  ssfin4  9997  insubm  18372  distop  22053  fctop  22062  cctop  22064  ntrin  22120  innei  22184  lly1stc  22555  txcnp  22679  isfild  22917  utoptop  23294  restmetu  23632  lecmi  29865  mdslj2i  30583  mdslmd1lem1  30588  mdslmd1lem2  30589  elpwincl1  30775  pnfneige0  31803  inelcarsg  32178  ballotlemfrc  32393  bnj1177  32886  bnj1311  32904  cldbnd  34442  neiin  34448  ontgval  34547  mblfinlem4  35744  pmodlem1  37787  pmodlem2  37788  pmod1i  37789  pmod2iN  37790  pmodl42N  37792  dochdmj1  39331  ssficl  41065  ntrclskb  41568  ntrclsk13  41570  ntrneik3  41595  ntrneik13  41597  ssinss1d  42485  icccncfext  43318  fourierdlem48  43585  fourierdlem49  43586  fourierdlem113  43650  caragendifcl  43942  omelesplit  43946  carageniuncllem2  43950  carageniuncl  43951