Metamath Proof Explorer

Theorem sslin

Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999)

Ref Expression
Assertion sslin 
|- ( A C_ B -> ( C i^i A ) C_ ( C i^i B ) )

Proof

Step Hyp Ref Expression
1 ssrin 
 |-  ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )
2 incom 
 |-  ( C i^i A ) = ( A i^i C )
3 incom 
 |-  ( C i^i B ) = ( B i^i C )
4 1 2 3 3sstr4g 
 |-  ( A C_ B -> ( C i^i A ) C_ ( C i^i B ) )