Theorem eqsstrrdi

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	eqsstrrdi.1	|- ( ph -> B = A )
	eqsstrrdi.2	|- B C_ C
Assertion	eqsstrrdi	|- ( ph -> A C_ C )

Proof

Step	Hyp	Ref	Expression
1		eqsstrrdi.1	|- ( ph -> B = A )
2		eqsstrrdi.2	|- B C_ C
3	1	eqcomd	|- ( ph -> A = B )
4	3 2	eqsstrdi	|- ( ph -> A C_ C )