Theorem sylan9req

Description: An equality transitivity deduction. (Contributed by NM, 23-Jun-2007)

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

Proof

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