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

Theorem ssind 3572
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 3570 . . 3  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
43biimpi 194 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  ->  A  C_  ( B  i^i  C ) )
51, 2, 4syl2anc 661 1  |-  ( ph  ->  A  C_  ( B  i^i  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    i^i cin 3325    C_ wss 3326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3333  df-ss 3340
This theorem is referenced by:  mreexexlem3d  14582  isacs1i  14593  rescabs  14744  funcres2c  14809  lsmmod  16170  gsumzres  16386  gsumzresOLD  16390  gsumzsubmcl  16400  gsumzsubmclOLD  16401  gsum2d  16461  gsum2dOLD  16462  issubdrg  16888  lspdisj  17204  mplind  17582  ntrin  18663  elcls  18675  neitr  18782  restcls  18783  lmss  18900  xkoinjcn  19258  trfg  19462  trust  19802  utoptop  19807  restutop  19810  isngp2  20187  lebnumii  20536  causs  20807  dvreslem  21382  c1lip3  21469  ssjo  24848  dmdbr5  25710  mdslj2i  25722  mdsl2bi  25725  mdslmd1lem2  25728  mdsymlem5  25809  neiin  28524  topmeet  28582  fnemeet2  28585  bnj1286  32007  pmod1i  33489  dihmeetlem1N  34932  dihglblem5apreN  34933  dochdmj1  35032  mapdin  35304  baerlem3lem2  35352  baerlem5alem2  35353  baerlem5blem2  35354
  Copyright terms: Public domain W3C validator