This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oveq123i

Description: Equality inference for operation value. (Contributed by FL, 11-Jul-2010)

Ref Expression
Hypotheses oveq123i.1 ⊢ A = C
oveq123i.2 ⊢ B = D
oveq123i.3 ⊢ F = G
Assertion oveq123i ⊢ A F B = C G D

Proof

Step Hyp Ref Expression
1 oveq123i.1 ⊢ A = C
2 oveq123i.2 ⊢ B = D
3 oveq123i.3 ⊢ F = G
4 1 2 oveq12i ⊢ A F B = C F D
5 3 oveqi ⊢ C F D = C G D
6 4 5 eqtri ⊢ A F B = C G D