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	⊢ ( 𝜑 → 𝐹 = 𝐺 )
	aoveq123d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
	aoveq123d.3	⊢ ( 𝜑 → 𝐶 = 𝐷 )
Assertion	aoveq123d	⊢ ( 𝜑 → (( 𝐴 𝐹 𝐶 )) = (( 𝐵 𝐺 𝐷 )) )

Proof

Step	Hyp	Ref	Expression
1		aoveq123d.1	⊢ ( 𝜑 → 𝐹 = 𝐺 )
2		aoveq123d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		aoveq123d.3	⊢ ( 𝜑 → 𝐶 = 𝐷 )
4	2 3	opeq12d	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐷 ⟩ )
5	1 4	afveq12d	⊢ ( 𝜑 → ( 𝐹 ''' ⟨ 𝐴 , 𝐶 ⟩ ) = ( 𝐺 ''' ⟨ 𝐵 , 𝐷 ⟩ ) )
6		df-aov	⊢ (( 𝐴 𝐹 𝐶 )) = ( 𝐹 ''' ⟨ 𝐴 , 𝐶 ⟩ )
7		df-aov	⊢ (( 𝐵 𝐺 𝐷 )) = ( 𝐺 ''' ⟨ 𝐵 , 𝐷 ⟩ )
8	5 6 7	3eqtr4g	⊢ ( 𝜑 → (( 𝐴 𝐹 𝐶 )) = (( 𝐵 𝐺 𝐷 )) )