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

Theorem ssind 3567
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 3565 . . 3  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
43biimpi 188 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  ->  A  C_  ( B  i^i  C ) )
51, 2, 4syl2anc 644 1  |-  ( ph  ->  A  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    i^i cin 3321    C_ wss 3322
This theorem is referenced by:  mreexexlem3d  13876  isacs1i  13887  rescabs  14038  funcres2c  14103  lsmmod  15312  gsumzres  15522  gsumzsubmcl  15528  gsum2d  15551  issubdrg  15898  lspdisj  16202  mplind  16567  ntrin  17130  elcls  17142  neitr  17249  restcls  17250  lmss  17367  xkoinjcn  17724  trfg  17928  trust  18264  utoptop  18269  restutop  18272  isngp2  18649  lebnumii  18996  causs  19256  dvreslem  19801  c1lip3  19888  ssjo  22954  dmdbr5  23816  mdslj2i  23828  mdsl2bi  23831  mdslmd1lem2  23834  mdsymlem5  23915  neiin  26349  topmeet  26407  fnemeet2  26410  bnj1286  29462  pmod1i  30719  dihmeetlem1N  32162  dihglblem5apreN  32163  dochdmj1  32262  mapdin  32534  baerlem3lem2  32582  baerlem5alem2  32583  baerlem5blem2  32584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator