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 )