Description: Equality deduction for operation value. (Contributed by NM, 13Mar1995) (Proof shortened by Andrew Salmon, 22Oct2011)
Ref  Expression  

Hypotheses  oveq1d.1   ( ph > A = B ) 

oveq12d.2   ( ph > C = D ) 

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

1  oveq1d.1   ( ph > A = B ) 

2  oveq12d.2   ( ph > C = D ) 

3  oveq12   ( ( A = B /\ C = D ) > ( A F C ) = ( B F D ) ) 

4  1 2 3  syl2anc   ( ph > ( A F C ) = ( B F D ) ) 