Description: Equality deduction for a binary relation. (Contributed by NM, 8Feb1996)
Ref  Expression  

Hypothesis  breq1d.1   ( ph > A = B ) 

Assertion  breq1d   ( ph > ( A R C <> B R C ) ) 
Step  Hyp  Ref  Expression 

1  breq1d.1   ( ph > A = B ) 

2  breq1   ( A = B > ( A R C <> B R C ) ) 

3  1 2  syl   ( ph > ( A R C <> B R C ) ) 