Theorem ssini 4136

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

This proof depends on syntax axioms:   ∧ wa 401   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  inv1  4347  uniin  4890  rnin  6136  cnvrescnv  6187  hartogslem1  9539  xptrrel  15138  fbasrn  24208  limciun  26219  hlimcaui  31843  chdmm1i  32084  chm0i  32097  ledii  32143  lejdii  32145  mayetes3i  32336  mdslj2i  32927  mdslmd2i  32937  sumdmdlem2  33026  sigapildsys  34841  ssoninhaus  37328  bj-disj2r  38033  bj-idres  38174  bj-rvecsscvec  38318  icomnfinre  46657  fouriersw  47334  sge0split  47512  numtowerdt  48009