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 AB
ssini.2 AC
Assertion ssini ABC

Proof

Step Hyp Ref Expression
1 ssini.1 AB
2 ssini.2 AC
3 1 2 pm3.2i ABAC
4 ssin ABACABC
5 3 4 mpbi ABC