Theorem eqsstrid

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

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

Proof

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