Description: Deduction adding difference to the right in a class equality. (Contributed by NM, 15Nov2002)
Ref  Expression  

Hypothesis  difeq1d.1   ( ph > A = B ) 

Assertion  difeq1d   ( ph > ( A \ C ) = ( B \ C ) ) 
Step  Hyp  Ref  Expression 

1  difeq1d.1   ( ph > A = B ) 

2  difeq1   ( A = B > ( A \ C ) = ( B \ C ) ) 

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