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	|- ( ph -> F = G )
	aoveq123d.2	|- ( ph -> A = B )
	aoveq123d.3	|- ( ph -> C = D )
Assertion	aoveq123d	|- ( ph -> (( A F C )) = (( B G D )) )

Proof

Step	Hyp	Ref	Expression
1		aoveq123d.1	|- ( ph -> F = G )
2		aoveq123d.2	|- ( ph -> A = B )
3		aoveq123d.3	|- ( ph -> C = D )
4	2 3	opeq12d	|- ( ph -> <. A , C >. = <. B , D >. )
5	1 4	afveq12d	|- ( ph -> ( F ''' <. A , C >. ) = ( G ''' <. B , D >. ) )
6		df-aov	|- (( A F C )) = ( F ''' <. A , C >. )
7		df-aov	|- (( B G D )) = ( G ''' <. B , D >. )
8	5 6 7	3eqtr4g	|- ( ph -> (( A F C )) = (( B G D )) )