Theorem sylan9eq

Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994) (Proof shortened by Andrew Salmon, 25-May-2011)

	Ref	Expression
Hypotheses	sylan9eq.1	$$⊢\phi \to A=B$$
	sylan9eq.2	$$⊢\psi \to B=C$$
Assertion	sylan9eq	$$⊢\left(\phi \wedge \psi \right)\to A=C$$

Proof

Step	Hyp	Ref	Expression
1		sylan9eq.1	$$⊢\phi \to A=B$$
2		sylan9eq.2	$$⊢\psi \to B=C$$
3		eqtr	$$⊢\left(A=B\wedge B=C\right)\to A=C$$
4	1 2 3	syl2an	$$⊢\left(\phi \wedge \psi \right)\to A=C$$