Metamath Proof Explorer


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 φF=G
aoveq123d.2 φA=B
aoveq123d.3 φC=D
Assertion aoveq123d φAFC=BGD

Proof

Step Hyp Ref Expression
1 aoveq123d.1 φF=G
2 aoveq123d.2 φA=B
3 aoveq123d.3 φC=D
4 2 3 opeq12d φAC=BD
5 1 4 afveq12d φF'''AC=G'''BD
6 df-aov AFC=F'''AC
7 df-aov BGD=G'''BD
8 5 6 7 3eqtr4g φAFC=BGD