Metamath Proof Explorer


Theorem oveq2i

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995)

Ref Expression
Hypothesis oveq1i.1 A = B
Assertion oveq2i C F A = C F B

Proof

Step Hyp Ref Expression
1 oveq1i.1 A = B
2 oveq2 A = B C F A = C F B
3 1 2 ax-mp C F A = C F B