Theorem ssini 4206

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

Syntax hints:   ∧ wa 398   ∩ cin 3933   ⊆ wss 3934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-in 3941  df-ss 3950

This theorem is referenced by:  inv1  4346  cnvrescnv  6045  hartogslem1  8998  xptrrel  14332  fbasrn  22484  limciun  24484  hlimcaui  29005  chdmm1i  29246  chm0i  29259  ledii  29305  lejdii  29307  mayetes3i  29498  mdslj2i  30089  mdslmd2i  30099  sumdmdlem2  30188  sigapildsys  31414  ssoninhaus  33789  bj-disj2r  34333  bj-idres  34444  bj-rvecsscvec  34577  icomnfinre  41817  fouriersw  42506  sge0split  42681