Theorem ssinss1 4246

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

Syntax hints:   → wi 4   ∩ cin 3950   ⊆ wss 3951

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  ssinss1d  4247  inss  4248  inindif  4375  wfrlem4OLD  8352  wfrlem5OLD  8353  fipwuni  9466  ssfin4  10350  insubm  18831  distop  23002  fctop  23011  cctop  23013  ntrin  23069  innei  23133  lly1stc  23504  txcnp  23628  isfild  23866  utoptop  24243  restmetu  24583  lecmi  31621  mdslj2i  32339  mdslmd1lem1  32344  mdslmd1lem2  32345  elpwincl1  32544  pnfneige0  33950  inelcarsg  34313  ballotlemfrc  34529  bnj1177  35020  bnj1311  35038  cldbnd  36327  neiin  36333  ontgval  36432  mblfinlem4  37667  pmodlem1  39848  pmodlem2  39849  pmod1i  39850  pmod2iN  39851  pmodl42N  39853  dochdmj1  41392  redvmptabs  42390  ssficl  43582  ntrclskb  44082  ntrclsk13  44084  ntrneik3  44109  ntrneik13  44111  sswfaxreg  45004  icccncfext  45902  fourierdlem48  46169  fourierdlem49  46170  fourierdlem113  46234  caragendifcl  46529  omelesplit  46533  carageniuncllem2  46537  carageniuncl  46538