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 )