Theorem addlidi 8250

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

Syntax hints:   = wceq 1373   ∈ wcel 2178  (class class class)co 5967  ℂcc 7958  0cc0 7960   + caddc 7963

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189  ax-1cn 8053  ax-icn 8055  ax-addcl 8056  ax-mulcl 8058  ax-addcom 8060  ax-i2m1 8065  ax-0id 8068

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  ine0  8501  inelr  8692  muleqadd  8776  0p1e1  9185  iap0  9295  num0h  9550  nummul1c  9587  decrmac  9596  decmul1  9602  fz0tp  10279  fz0to4untppr  10281  fzo0to3tp  10385  rei  11325  imi  11326  resqrexlemover  11436  ef01bndlem  12182  5ndvds3  12360  dec5dvds2  12851  2exp11  12874  2exp16  12875  efhalfpi  15386  sinq34lt0t  15418  ex-fac  15864