Theorem ssinss1 4212

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

Syntax hints:   → wi 4   ∩ cin 3916   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  ssinss1d  4213  inss  4214  inindif  4341  fipwuni  9384  ssfin4  10270  insubm  18752  distop  22889  fctop  22898  cctop  22900  ntrin  22955  innei  23019  lly1stc  23390  txcnp  23514  isfild  23752  utoptop  24129  restmetu  24465  lecmi  31538  mdslj2i  32256  mdslmd1lem1  32261  mdslmd1lem2  32262  elpwincl1  32461  pnfneige0  33948  inelcarsg  34309  ballotlemfrc  34525  bnj1177  35003  bnj1311  35021  cldbnd  36321  neiin  36327  ontgval  36426  mblfinlem4  37661  pmodlem1  39847  pmodlem2  39848  pmod1i  39849  pmod2iN  39850  pmodl42N  39852  dochdmj1  41391  redvmptabs  42355  ssficl  43565  ntrclskb  44065  ntrclsk13  44067  ntrneik3  44092  ntrneik13  44094  sswfaxreg  44984  icccncfext  45892  fourierdlem48  46159  fourierdlem49  46160  fourierdlem113  46224  caragendifcl  46519  omelesplit  46523  carageniuncllem2  46527  carageniuncl  46528