Description: An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24Nov2003)
Ref  Expression  

Hypotheses  ssini.1   A C_ B 

ssini.2   A C_ C 

Assertion  ssini   A C_ ( B i^i C ) 
Step  Hyp  Ref  Expression 

1  ssini.1   A C_ B 

2  ssini.2   A C_ C 

3  1 2  pm3.2i   ( A C_ B /\ A C_ C ) 
4  ssin   ( ( A C_ B /\ A C_ C ) <> A C_ ( B i^i C ) ) 

5  3 4  mpbi   A C_ ( B i^i C ) 