Description: Equality deduction for a binary relation. (Contributed by NM, 8Feb1996) (Proof shortened by Andrew Salmon, 9Jul2011)
Ref  Expression  

Hypotheses  breq1d.1   ( ph > A = B ) 

breq12d.2   ( ph > C = D ) 

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

1  breq1d.1   ( ph > A = B ) 

2  breq12d.2   ( ph > C = D ) 

3  breq12   ( ( A = B /\ C = D ) > ( A R C <> B R D ) ) 

4  1 2 3  syl2anc   ( ph > ( A R C <> B R D ) ) 