Theorem ssinss1 4196

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

Syntax hints:   → wi 4   ∩ cin 3898   ⊆ wss 3899

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906  df-ss 3916

This theorem is referenced by:  ssinss1d  4197  inss  4198  inindif  4325  fipwuni  9327  ssfin4  10218  insubm  18741  distop  22937  fctop  22946  cctop  22948  ntrin  23003  innei  23067  lly1stc  23438  txcnp  23562  isfild  23800  utoptop  24176  restmetu  24512  lecmi  31626  mdslj2i  32344  mdslmd1lem1  32349  mdslmd1lem2  32350  elpwincl1  32549  pnfneige0  34057  inelcarsg  34417  ballotlemfrc  34633  bnj1177  35111  bnj1311  35129  cldbnd  36469  neiin  36475  ontgval  36574  mblfinlem4  37800  pmodlem1  40045  pmodlem2  40046  pmod1i  40047  pmod2iN  40048  pmodl42N  40050  dochdmj1  41589  redvmptabs  42557  ssficl  43752  ntrclskb  44252  ntrclsk13  44254  ntrneik3  44279  ntrneik13  44281  sswfaxreg  45170  icccncfext  46073  fourierdlem48  46340  fourierdlem49  46341  fourierdlem113  46405  caragendifcl  46700  omelesplit  46704  carageniuncllem2  46708  carageniuncl  46709