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

Theorem ssind 3668
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 3666 . . 3  |-  ( ( A  C_  B  /\  A  C_  C )  <->  A  C_  ( B  i^i  C ) )
43biimpi 199 . 2  |-  ( ( A  C_  B  /\  A  C_  C )  ->  A  C_  ( B  i^i  C ) )
51, 2, 4syl2anc 671 1  |-  ( ph  ->  A  C_  ( B  i^i  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    i^i cin 3415    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430
This theorem is referenced by:  mreexexlem3d  15601  isacs1i  15612  rescabs  15787  funcres2c  15855  lsmmod  17374  gsumzres  17592  gsumzsubmcl  17600  gsum2d  17653  issubdrg  18082  lspdisj  18397  mplind  18774  ntrin  20125  elcls  20138  neitr  20245  restcls  20246  lmss  20363  xkoinjcn  20751  trfg  20955  trust  21293  utoptop  21298  restutop  21301  isngp2  21660  lebnumii  22046  causs  22317  dvreslem  22913  c1lip3  23000  ssjo  27149  dmdbr5  28010  mdslj2i  28022  mdsl2bi  28025  mdslmd1lem2  28028  mdsymlem5  28109  bnj1286  29877  mclsind  30257  neiin  31037  topmeet  31069  fnemeet2  31072  pmod1i  33458  dihmeetlem1N  34903  dihglblem5apreN  34904  dochdmj1  35003  mapdin  35275  baerlem3lem2  35323  baerlem5alem2  35324  baerlem5blem2  35325  trrelind  36302  nzin  36711  islptre  37737  limccog  37738  limcresiooub  37761  limcresioolb  37762  fourierdlem48  38056  fourierdlem49  38057  fourierdlem113  38121
  Copyright terms: Public domain W3C validator