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

Theorem ss2in 3572
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 3570 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 sslin 3571 . 2  |-  ( C 
C_  D  ->  ( B  i^i  C )  C_  ( B  i^i  D ) )
31, 2sylan9ss 3364 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 3322    C_ wss 3323
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 2419
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 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337
This theorem is referenced by:  disjxiun  4284  undom  7391  strlemor1  14257  strleun  14260  dprdss  16516  dprd2da  16531  ablfac1b  16561  tgcl  18554  innei  18709  hausnei2  18937  bwth  18993  fbssfi  19390  fbunfip  19422  fgcl  19431  blin2  19984  vdgrun  23539  vdgrfiun  23540  5oai  25032  mayetes3i  25101  mdsl0  25682  ismblfin  28403  neibastop1  28551  heibor1lem  28679  pl42lem2N  33517  pl42lem3N  33518
  Copyright terms: Public domain W3C validator