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 C_ B
	ssini.2	|- A C_ C
Assertion	ssini	|- A C_ ( B i^i C )

Proof

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 )