Theorem sylan9ss

Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004) (Proof shortened by Andrew Salmon, 14-Jun-2011)

	Ref	Expression
Hypotheses	sylan9ss.1	|- ( ph -> A C_ B )
	sylan9ss.2	|- ( ps -> B C_ C )
Assertion	sylan9ss	|- ( ( ph /\ ps ) -> A C_ C )

Proof

Step	Hyp	Ref	Expression
1		sylan9ss.1	|- ( ph -> A C_ B )
2		sylan9ss.2	|- ( ps -> B C_ C )
3		sstr	|- ( ( A C_ B /\ B C_ C ) -> A C_ C )
4	1 2 3	syl2an	|- ( ( ph /\ ps ) -> A C_ C )