Description: Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31Dec2019)
Ref  Expression  

Hypothesis  eceq1d.1   ( ph > A = B ) 

Assertion  eceq1d   ( ph > [ A ] C = [ B ] C ) 
Step  Hyp  Ref  Expression 

1  eceq1d.1   ( ph > A = B ) 

2  eceq1   ( A = B > [ A ] C = [ B ] C ) 

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