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

Theorem ssind 3393
Description: A deduction showing that the a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
ssind.1  |-  ( ph  ->  A  C_  B )
ssind.2  |-  ( ph  ->  A  C_  C )
Assertion
Ref Expression
ssind  |-  ( ph  ->  A  C_  ( B  i^i  C ) )

Proof of Theorem ssind
StepHypRef Expression
1 ssind.1 . 2  |-  ( ph  ->  A  C_  B )
2 ssind.2 . 2  |-  ( ph  ->  A  C_  C )
3 ssin 3391 . . 3  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
43biimpi 186 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  ->  A  C_  ( B  i^i  C ) )
51, 2, 4syl2anc 642 1  |-  ( ph  ->  A  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  mreexexlem3d  13548  isacs1i  13559  rescabs  13710  funcres2c  13775  lsmmod  14984  gsumzres  15194  gsumzsubmcl  15200  gsum2d  15223  issubdrg  15570  lspdisj  15878  mplind  16243  ntrin  16798  elcls  16810  restcls  16911  lmss  17026  xkoinjcn  17381  trfg  17586  isngp2  18119  lebnumii  18464  causs  18724  dvreslem  19259  c1lip3  19346  ssjo  22026  dmdbr5  22888  mdslj2i  22900  mdsl2bi  22903  mdslmd1lem2  22906  mdsymlem5  22987  neiin  26250  topmeet  26313  fnemeet2  26316  bnj1286  29049  pmod1i  30037  dihmeetlem1N  31480  dihglblem5apreN  31481  dochdmj1  31580  mapdin  31852  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator