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

Theorem ss2in 3707
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 3705 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 sslin 3706 . 2  |-  ( C 
C_  D  ->  ( B  i^i  C )  C_  ( B  i^i  D ) )
31, 2sylan9ss 3499 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 3457    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-in 3465  df-ss 3472
This theorem is referenced by:  disjxiun  4430  undom  7603  strlemor1  14596  strleun  14599  dprdss  16944  dprd2da  16959  ablfac1b  16989  tgcl  19337  innei  19492  hausnei2  19720  bwth  19776  fbssfi  20204  fbunfip  20236  fgcl  20245  blin2  20798  vdgrun  24766  vdgrfiun  24767  5oai  26444  mayetes3i  26513  mdsl0  27094  ismblfin  30023  neibastop1  30145  heibor1lem  30273  pl42lem2N  35406  pl42lem3N  35407
  Copyright terms: Public domain W3C validator