Theorem sylan9eqr

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994)

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

Proof

Step	Hyp	Ref	Expression
1		sylan9eqr.1	|- ( ph -> A = B )
2		sylan9eqr.2	|- ( ps -> B = C )
3	1 2	sylan9eq	|- ( ( ph /\ ps ) -> A = C )
4	3	ancoms	|- ( ( ps /\ ph ) -> A = C )