Theorem ssinss1 4236

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

Syntax hints:   → wi 4   ∩ cin 3946   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  inss  4237  wfrlem4OLD  8314  wfrlem5OLD  8315  fipwuni  9423  ssfin4  10307  insubm  18735  distop  22718  fctop  22727  cctop  22729  ntrin  22785  innei  22849  lly1stc  23220  txcnp  23344  isfild  23582  utoptop  23959  restmetu  24299  lecmi  31122  mdslj2i  31840  mdslmd1lem1  31845  mdslmd1lem2  31846  elpwincl1  32030  pnfneige0  33229  inelcarsg  33608  ballotlemfrc  33823  bnj1177  34315  bnj1311  34333  cldbnd  35514  neiin  35520  ontgval  35619  mblfinlem4  36831  pmodlem1  39020  pmodlem2  39021  pmod1i  39022  pmod2iN  39023  pmodl42N  39025  dochdmj1  40564  ssficl  42622  ntrclskb  43122  ntrclsk13  43124  ntrneik3  43149  ntrneik13  43151  ssinss1d  44036  icccncfext  44901  fourierdlem48  45168  fourierdlem49  45169  fourierdlem113  45233  caragendifcl  45528  omelesplit  45532  carageniuncllem2  45536  carageniuncl  45537