Metamath Proof Explorer

Theorem ssini

Description: An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003)

Ref Expression
Hypotheses ssini.1 A B
ssini.2 A C
Assertion ssini A B C


Step Hyp Ref Expression
1 ssini.1 A B
2 ssini.2 A C
3 1 2 pm3.2i A B A C
4 ssin A B A C A B C
5 3 4 mpbi A B C