Theorem ssinss1 4221

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

Syntax hints:   → wi 4   ∩ cin 3925   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  ssinss1d  4222  inss  4223  inindif  4350  wfrlem4OLD  8326  wfrlem5OLD  8327  fipwuni  9438  ssfin4  10324  insubm  18796  distop  22933  fctop  22942  cctop  22944  ntrin  22999  innei  23063  lly1stc  23434  txcnp  23558  isfild  23796  utoptop  24173  restmetu  24509  lecmi  31583  mdslj2i  32301  mdslmd1lem1  32306  mdslmd1lem2  32307  elpwincl1  32506  pnfneige0  33982  inelcarsg  34343  ballotlemfrc  34559  bnj1177  35037  bnj1311  35055  cldbnd  36344  neiin  36350  ontgval  36449  mblfinlem4  37684  pmodlem1  39865  pmodlem2  39866  pmod1i  39867  pmod2iN  39868  pmodl42N  39870  dochdmj1  41409  redvmptabs  42403  ssficl  43593  ntrclskb  44093  ntrclsk13  44095  ntrneik3  44120  ntrneik13  44122  sswfaxreg  45012  icccncfext  45916  fourierdlem48  46183  fourierdlem49  46184  fourierdlem113  46248  caragendifcl  46543  omelesplit  46547  carageniuncllem2  46551  carageniuncl  46552