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

Theorem ssini 3682
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 455 . 2  |-  ( A 
C_  B  /\  A  C_  C )
4 ssin 3681 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
53, 4mpbi 208 1  |-  A  C_  ( B  i^i  C )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    i^i cin 3436    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3444  df-ss 3451
This theorem is referenced by:  inv1  3773  hartogslem1  7868  fbasrn  19590  limciun  21503  hlimcaui  24792  chdmm1i  25033  chm0i  25046  ledii  25092  lejdii  25094  mayetes3i  25286  mdslj2i  25877  mdslmd2i  25887  sumdmdlem2  25976  measunl  26776  ssoninhaus  28439
  Copyright terms: Public domain W3C validator