Theorem ssini 4232

Description: An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003.)

Hypotheses

Ref	Expression
ssini.1	⊢ 𝐴 ⊆ 𝐵
ssini.2	⊢ 𝐴 ⊆ 𝐶

Assertion

Ref	Expression
ssini	⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶)

Proof of Theorem ssini

Step	Hyp	Ref	Expression
1		ssini.1	. . 3 ⊢ 𝐴 ⊆ 𝐵
2		ssini.2	. . 3 ⊢ 𝐴 ⊆ 𝐶
3	1, 2	pm3.2i 469	. 2 ⊢ (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶)
4		ssin 4231	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
5	3, 4	mpbi 229	1 ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶)

Syntax hints:   ∧ wa 394   ∩ cin 3948   ⊆ wss 3949

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 3956  df-ss 3966

This theorem is referenced by:  inv1  4395  cnvrescnv  6195  hartogslem1  9541  xptrrel  14933  fbasrn  23610  limciun  25645  hlimcaui  30754  chdmm1i  30995  chm0i  31008  ledii  31054  lejdii  31056  mayetes3i  31247  mdslj2i  31838  mdslmd2i  31848  sumdmdlem2  31937  sigapildsys  33456  ssoninhaus  35638  bj-disj2r  36214  bj-idres  36346  bj-rvecsscvec  36490  icomnfinre  44565  fouriersw  45247  sge0split  45425