Description: Equality deduction for operation value. (Contributed by NM, 13Mar1995)
Ref  Expression  

Hypothesis  oveq1d.1   ( ph > A = B ) 

Assertion  oveq1d   ( ph > ( A F C ) = ( B F C ) ) 
Step  Hyp  Ref  Expression 

1  oveq1d.1   ( ph > A = B ) 

2  oveq1   ( A = B > ( A F C ) = ( B F C ) ) 

3  1 2  syl   ( ph > ( A F C ) = ( B F C ) ) 