Theorem ssini 4195

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

This proof depends on syntax axioms:   ∧ wa 401   ∩ cin 3907   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-in 3915  df-ss 3925

This theorem is used by:  inv1  4358  uniin  4901  rnin  6148  cnvrescnv  6199  hartogslem1  9514  xptrrel  15043  fbasrn  24078  limciun  26090  hlimcaui  31625  chdmm1i  31866  chm0i  31879  ledii  31925  lejdii  31927  mayetes3i  32118  mdslj2i  32709  mdslmd2i  32719  sumdmdlem2  32808  sigapildsys  34583  ssoninhaus  36999  bj-disj2r  37704  bj-idres  37844  bj-rvecsscvec  37988  icomnfinre  46308  fouriersw  46985  sge0split  47163  nthrucw  47647