Theorem ssini 4175

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

Syntax hints:   ∧ wa 396   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-in 3897  df-ss 3907

This theorem is referenced by:  inv1  4333  cnvrescnv  6153  hartogslem1  9454  xptrrel  14940  fbasrn  23874  limciun  25886  hlimcaui  31332  chdmm1i  31573  chm0i  31586  ledii  31632  lejdii  31634  mayetes3i  31825  mdslj2i  32416  mdslmd2i  32426  sumdmdlem2  32515  sigapildsys  34353  ssoninhaus  36683  bj-disj2r  37388  bj-idres  37527  bj-rvecsscvec  37671  icomnfinre  46004  fouriersw  46681  sge0split  46859  nthrucw  47338