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

Theorem ss2in 3396
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 3394 . 2  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
2 sslin 3395 . 2  |-  ( C 
C_  D  ->  ( B  i^i  C )  C_  ( B  i^i  D ) )
31, 2sylan9ss 3192 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  i^i  C
)  C_  ( B  i^i  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  disjxiun  4020  undom  6950  strlemor1  13235  strleun  13238  dprdss  15264  dprd2da  15277  ablfac1b  15305  tgcl  16707  innei  16862  hausnei2  17081  fbssfi  17532  fbunfip  17564  fgcl  17573  blin2  17975  5oai  22240  mayetes3i  22309  mdsl0  22890  vdgrun  23893  int2pre  25237  neibastop1  26308  heibor1lem  26533  pl42lem2N  30169  pl42lem3N  30170
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator