Theorem ssini 4192

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 470	. 2 ⊢ (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶)
4		ssin 4191	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶))
5	3, 4	mpbi 230	1 ⊢ 𝐴 ⊆ (𝐵 ∩ 𝐶)

Syntax hints:   ∧ wa 395   ∩ cin 3900   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  inv1  4350  cnvrescnv  6153  hartogslem1  9447  xptrrel  14903  fbasrn  23828  limciun  25851  hlimcaui  31311  chdmm1i  31552  chm0i  31565  ledii  31611  lejdii  31613  mayetes3i  31804  mdslj2i  32395  mdslmd2i  32405  sumdmdlem2  32494  sigapildsys  34319  ssoninhaus  36642  bj-disj2r  37229  bj-idres  37361  bj-rvecsscvec  37505  icomnfinre  45794  fouriersw  46471  sge0split  46649  nthrucw  47126