Metamath Proof Explorer

Theorem oveq12i

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Hypotheses oveq1i.1 
|- A = B
oveq12i.2 
|- C = D
Assertion oveq12i 
|- ( A F C ) = ( B F D )

Proof

Step Hyp Ref Expression
1 oveq1i.1 
 |-  A = B
2 oveq12i.2 
 |-  C = D
3 oveq12 
 |-  ( ( A = B /\ C = D ) -> ( A F C ) = ( B F D ) )
4 1 2 3 mp2an 
 |-  ( A F C ) = ( B F D )