Theorem aoveq123d

Description: Equality deduction for operation value, analogous to oveq123d . (Contributed by Alexander van der Vekens, 26-May-2017)

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

Proof

Step	Hyp	Ref	Expression
1		aoveq123d.1	$$⊢\phi \to F=G$$
2		aoveq123d.2	$$⊢\phi \to A=B$$
3		aoveq123d.3	$$⊢\phi \to C=D$$
4	2 3	opeq12d	$$⊢\phi \to ⟨A,C⟩=⟨B,D⟩$$
5	1 4	afveq12d	$$⊢\phi \to \left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,C⟩\right)=\left(G\mathrm{\text{'}\text{'}\text{'}}⟨B,D⟩\right)$$
6		df-aov	$$⊢((AFC))=\left(F\mathrm{\text{'}\text{'}\text{'}}⟨A,C⟩\right)$$
7		df-aov	$$⊢((BGD))=\left(G\mathrm{\text{'}\text{'}\text{'}}⟨B,D⟩\right)$$
8	5 6 7	3eqtr4g	$$⊢\phi \to ((AFC))=((BGD))$$