Theorem addlidi 8327

Description: 0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)

Hypothesis

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
addlidi	⊢ (0 + 𝐴) = 𝐴

Proof of Theorem addlidi

Step	Hyp	Ref	Expression
1		mul.1	. 2 ⊢ 𝐴 ∈ ℂ
2		addlid 8323	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (0 + 𝐴) = 𝐴

Syntax hints:   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035  0cc0 8037   + caddc 8040

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2212  ax-1cn 8130  ax-icn 8132  ax-addcl 8133  ax-mulcl 8135  ax-addcom 8137  ax-i2m1 8142  ax-0id 8145

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-clel 2226

This theorem is referenced by:  ine0  8578  inelr  8769  muleqadd  8853  0p1e1  9262  iap0  9372  num0h  9627  nummul1c  9664  decrmac  9673  decmul1  9679  fz0tp  10362  fz0to4untppr  10364  fzo0to3tp  10470  cats1fvn  11354  rei  11482  imi  11483  resqrexlemover  11593  ef01bndlem  12340  5ndvds3  12518  dec5dvds2  13009  2exp11  13032  2exp16  13033  efhalfpi  15552  sinq34lt0t  15584  ex-fac  16381