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

Theorem ssind 3469
Description: A deduction showing that 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 3467 . . 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 3227    C_ wss 3228
This theorem is referenced by:  mreexexlem3d  13647  isacs1i  13658  rescabs  13809  funcres2c  13874  lsmmod  15083  gsumzres  15293  gsumzsubmcl  15299  gsum2d  15322  issubdrg  15669  lspdisj  15977  mplind  16342  ntrin  16904  elcls  16916  restcls  17017  lmss  17132  xkoinjcn  17487  trfg  17688  isngp2  18221  lebnumii  18568  causs  18828  dvreslem  19363  c1lip3  19450  ssjo  22140  dmdbr5  23002  mdslj2i  23014  mdsl2bi  23017  mdslmd1lem2  23020  mdsymlem5  23101  utoptop  23538  restutop  23541  neiin  25574  topmeet  25637  fnemeet2  25640  bnj1286  28811  pmod1i  30106  dihmeetlem1N  31549  dihglblem5apreN  31550  dochdmj1  31649  mapdin  31921  baerlem3lem2  31969  baerlem5alem2  31970  baerlem5blem2  31971
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator