Theorem oveq123d

Description: Equality deduction for operation value. (Contributed by FL, 22-Dec-2008)

	Ref	Expression
Hypotheses	oveq123d.1	$$⊢\phi \to F=G$$
	oveq123d.2	$$⊢\phi \to A=B$$
	oveq123d.3	$$⊢\phi \to C=D$$
Assertion	oveq123d	$$⊢\phi \to AFC=BGD$$

Proof

Step	Hyp	Ref	Expression
1		oveq123d.1	$$⊢\phi \to F=G$$
2		oveq123d.2	$$⊢\phi \to A=B$$
3		oveq123d.3	$$⊢\phi \to C=D$$
4	1	oveqd	$$⊢\phi \to AFC=AGC$$
5	2 3	oveq12d	$$⊢\phi \to AGC=BGD$$
6	4 5	eqtrd	$$⊢\phi \to AFC=BGD$$