Theorem ssinss1 4096

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

Syntax hints:   → wi 4   ∩ cin 3824   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-in 3832  df-ss 3839

This theorem is referenced by:  inss  4097  wfrlem4  7754  wfrlem4OLD  7755  wfrlem5  7756  fipwuni  8677  ssfin4  9522  distop  21297  fctop  21306  cctop  21308  ntrin  21363  innei  21427  lly1stc  21798  txcnp  21922  isfild  22160  utoptop  22536  restmetu  22873  lecmi  29150  mdslj2i  29868  mdslmd1lem1  29873  mdslmd1lem2  29874  elpwincl1  30050  pnfneige0  30795  inelcarsg  31171  ballotlemfrc  31387  bnj1177  31884  bnj1311  31902  cldbnd  33135  neiin  33141  ontgval  33239  mblfinlem4  34321  pmodlem1  36375  pmodlem2  36376  pmod1i  36377  pmod2iN  36378  pmodl42N  36380  dochdmj1  37919  ssficl  39235  ntrclskb  39727  ntrclsk13  39729  ntrneik3  39754  ntrneik13  39756  ssinss1d  40673  icccncfext  41546  fourierdlem48  41816  fourierdlem49  41817  fourierdlem113  41881  caragendifcl  42173  omelesplit  42177  carageniuncllem2  42181  carageniuncl  42182