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

Theorem ss2in 3677
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 3675 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 sslin 3676 . 2  |-  ( C 
C_  D  ->  ( B  i^i  C )  C_  ( B  i^i  D ) )
31, 2sylan9ss 3469 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 3427    C_ wss 3428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3072  df-in 3435  df-ss 3442
This theorem is referenced by:  disjxiun  4389  undom  7501  strlemor1  14369  strleun  14372  dprdss  16633  dprd2da  16648  ablfac1b  16678  tgcl  18692  innei  18847  hausnei2  19075  bwth  19131  fbssfi  19528  fbunfip  19560  fgcl  19569  blin2  20122  vdgrun  23708  vdgrfiun  23709  5oai  25201  mayetes3i  25270  mdsl0  25851  ismblfin  28572  neibastop1  28720  heibor1lem  28848  pl42lem2N  33932  pl42lem3N  33933
  Copyright terms: Public domain W3C validator