Theorem ssind

Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

	Ref	Expression
Hypotheses	ssind.1	|- ( ph -> A C_ B )
	ssind.2	|- ( ph -> A C_ C )
Assertion	ssind	|- ( ph -> A C_ ( B i^i C ) )

Proof

Step	Hyp	Ref	Expression
1		ssind.1	|- ( ph -> A C_ B )
2		ssind.2	|- ( ph -> A C_ C )
3	1 2	jca	|- ( ph -> ( A C_ B /\ A C_ C ) )
4		ssin	|- ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )
5	3 4	sylib	|- ( ph -> A C_ ( B i^i C ) )