Theorem addid1 7900

Description: 0 is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.)

Assertion

Ref	Expression
addid1	⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Proof of Theorem addid1

Step	Hyp	Ref	Expression
1		ax-0id 7728	1 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618  0cc0 7620   + caddc 7623

This theorem was proved from axioms:  ax-0id 7728

This theorem is referenced by:  addid2  7901  00id  7903  addid1i  7904  addid1d  7911  addcan2  7943  subid  7981  subid1  7982  addid0  8135  shftval3  10599  reim0  10633  fsum3cvg  11147  summodclem2a  11150