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

Theorem ssini 3646
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  |-  A  C_  B
ssini.2  |-  A  C_  C
Assertion
Ref Expression
ssini  |-  A  C_  ( B  i^i  C )

Proof of Theorem ssini
StepHypRef Expression
1 ssini.1 . . 3  |-  A  C_  B
2 ssini.2 . . 3  |-  A  C_  C
31, 2pm3.2i 462 . 2  |-  ( A 
C_  B  /\  A  C_  C )
4 ssin 3645 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
53, 4mpbi 213 1  |-  A  C_  ( B  i^i  C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 376    i^i cin 3389    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-in 3397  df-ss 3404
This theorem is referenced by:  inv1  3764  hartogslem1  8075  xptrrel  13119  fbasrn  20977  limciun  22928  hlimcaui  26970  chdmm1i  27211  chm0i  27224  ledii  27270  lejdii  27272  mayetes3i  27463  mdslj2i  28054  mdslmd2i  28064  sumdmdlem2  28153  sigapildsys  29058  ssoninhaus  31179  fouriersw  38207  sge0split  38365
  Copyright terms: Public domain W3C validator