Theorem ssini 4185

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

This proof depends on syntax axioms:   ∧ wa 401   ∩ cin 3898   ⊆ wss 3899

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  inv1  4348  uniin  4891  rnin  6135  cnvrescnv  6187  hartogslem1  9520  xptrrel  15113  fbasrn  24183  limciun  26194  hlimcaui  31820  chdmm1i  32061  chm0i  32074  ledii  32120  lejdii  32122  mayetes3i  32313  mdslj2i  32904  mdslmd2i  32914  sumdmdlem2  33003  sigapildsys  34777  ssoninhaus  37206  bj-disj2r  37911  bj-idres  38049  bj-rvecsscvec  38193  icomnfinre  46508  fouriersw  47185  sge0split  47363  numtowerdt  47860