Metamath Proof Explorer

Theorem ss2in

Description: Intersection of subclasses. (Contributed by NM, 5-May-2000)

Ref Expression
Assertion ss2in 
|- ( ( A C_ B /\ C C_ D ) -> ( A i^i C ) C_ ( B i^i D ) )

Proof

Step Hyp Ref Expression
1 ssrin 
 |-  ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )
2 sslin 
 |-  ( C C_ D -> ( B i^i C ) C_ ( B i^i D ) )
3 1 2 sylan9ss 
 |-  ( ( A C_ B /\ C C_ D ) -> ( A i^i C ) C_ ( B i^i D ) )