Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27May2016)
Ref  Expression  

Hypothesis  muld.1   ( ph > A e. CC ) 

Assertion  addid1d   ( ph > ( A + 0 ) = A ) 
Step  Hyp  Ref  Expression 

1  muld.1   ( ph > A e. CC ) 

2  addid1   ( A e. CC > ( A + 0 ) = A ) 

3  1 2  syl   ( ph > ( A + 0 ) = A ) 