Theorem addlidi 8257

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 8253	. 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ (0 + 𝐴) = 𝐴

Syntax hints:   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965  0cc0 7967   + caddc 7970

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-17 1552  ax-ial 1560  ax-ext 2191  ax-1cn 8060  ax-icn 8062  ax-addcl 8063  ax-mulcl 8065  ax-addcom 8067  ax-i2m1 8072  ax-0id 8075

This theorem depends on definitions:  df-bi 117  df-cleq 2202  df-clel 2205

This theorem is referenced by:  ine0  8508  inelr  8699  muleqadd  8783  0p1e1  9192  iap0  9302  num0h  9557  nummul1c  9594  decrmac  9603  decmul1  9609  fz0tp  10286  fz0to4untppr  10288  fzo0to3tp  10392  cats1fvn  11262  rei  11376  imi  11377  resqrexlemover  11487  ef01bndlem  12233  5ndvds3  12411  dec5dvds2  12902  2exp11  12925  2exp16  12926  efhalfpi  15438  sinq34lt0t  15470  ex-fac  16002