Theorem ssini 4158

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

Syntax hints:   ∧ wa 399   ∩ cin 3880   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  inv1  4302  cnvrescnv  6019  hartogslem1  8990  xptrrel  14331  fbasrn  22489  limciun  24497  hlimcaui  29019  chdmm1i  29260  chm0i  29273  ledii  29319  lejdii  29321  mayetes3i  29512  mdslj2i  30103  mdslmd2i  30113  sumdmdlem2  30202  sigapildsys  31531  ssoninhaus  33909  bj-disj2r  34464  bj-idres  34575  bj-rvecsscvec  34718  icomnfinre  42189  fouriersw  42873  sge0split  43048