Theorem addlidi 8412

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

Syntax hints:   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121  0cc0 8123   + caddc 8126

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214  ax-1cn 8216  ax-icn 8218  ax-addcl 8219  ax-mulcl 8221  ax-addcom 8223  ax-i2m1 8228  ax-0id 8231

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  ine0  8663  inelr  8854  muleqadd  8938  0p1e1  9347  iap0  9457  num0h  9716  nummul1c  9753  decrmac  9762  decmul1  9768  fz0tp  10452  fz0to4untppr  10454  fzo0to3tp  10560  cats1fvn  11449  rei  11577  imi  11578  resqrexlemover  11688  ef01bndlem  12435  5ndvds3  12613  dec5dvds2  13104  2exp11  13127  2exp16  13128  efhalfpi  15651  sinq34lt0t  15683  ex-fac  16483