Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssini Structured version   Visualization version   GIF version

Theorem ssini 3979
 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
StepHypRef Expression
1 ssini.1 . . 3 𝐴𝐵
2 ssini.2 . . 3 𝐴𝐶
31, 2pm3.2i 470 . 2 (𝐴𝐵𝐴𝐶)
4 ssin 3978 . 2 ((𝐴𝐵𝐴𝐶) ↔ 𝐴 ⊆ (𝐵𝐶))
53, 4mpbi 220 1 𝐴 ⊆ (𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 383   ∩ cin 3714   ⊆ wss 3715 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729 This theorem is referenced by:  inv1  4113  hartogslem1  8614  xptrrel  13940  fbasrn  21909  limciun  23877  hlimcaui  28423  chdmm1i  28666  chm0i  28679  ledii  28725  lejdii  28727  mayetes3i  28918  mdslj2i  29509  mdslmd2i  29519  sumdmdlem2  29608  sigapildsys  30555  ssoninhaus  32774  bj-disj2r  33337  idinxpres  34430  icomnfinre  40300  fouriersw  40969  sge0split  41147
 Copyright terms: Public domain W3C validator