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

Theorem ss2in 3718
Description: Intersection of subclasses. (Contributed by NM, 5-May-2000.)
Assertion
Ref Expression
ss2in  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  i^i  C
)  C_  ( B  i^i  D ) )

Proof of Theorem ss2in
StepHypRef Expression
1 ssrin 3716 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 sslin 3717 . 2  |-  ( C 
C_  D  ->  ( B  i^i  C )  C_  ( B  i^i  D ) )
31, 2sylan9ss 3510 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  i^i  C
)  C_  ( B  i^i  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    i^i cin 3468    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ss 3483
This theorem is referenced by:  disjxiun  4437  undom  7595  strlemor1  14571  strleun  14574  dprdss  16859  dprd2da  16874  ablfac1b  16904  tgcl  19230  innei  19385  hausnei2  19613  bwth  19669  fbssfi  20066  fbunfip  20098  fgcl  20107  blin2  20660  vdgrun  24563  vdgrfiun  24564  5oai  26105  mayetes3i  26174  mdsl0  26755  ismblfin  29483  neibastop1  29631  heibor1lem  29759  icccncfext  31045  pl42lem2N  34651  pl42lem3N  34652
  Copyright terms: Public domain W3C validator