Theorem eqsstrrid

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004)

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

Proof

Step	Hyp	Ref	Expression
1		eqsstrrid.1	|- B = A
2		eqsstrrid.2	|- ( ph -> B C_ C )
3	1	eqcomi	|- A = B
4	3 2	eqsstrid	|- ( ph -> A C_ C )