Theorem addid2i 10820

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

Hypothesis

Ref	Expression
mul.1	⊢ 𝐴 ∈ ℂ

Assertion

Ref	Expression
addid2i	⊢ (0 + 𝐴) = 𝐴

Proof of Theorem addid2i

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

Syntax hints:   = wceq 1531   ∈ wcel 2108  (class class class)co 7148  ℂcc 10527  0cc0 10529   + caddc 10532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-po 5467  df-so 5468  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-ltxr 10672

This theorem is referenced by:  ine0  11067  muleqadd  11276  inelr  11620  nnne0  11663  0p1e1  11751  num0h  12102  nummul1c  12139  decrmac  12148  fz0tp  13000  fz0to4untppr  13002  fzo0to3tp  13115  cats1fvn  14212  rei  14507  imi  14508  ef01bndlem  15529  gcdaddmlem  15864  dec5dvds2  16393  2exp16  16416  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem1  16456  1259lem2  16457  1259lem3  16458  1259lem4  16459  1259lem5  16460  2503lem1  16462  2503lem2  16463  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001prm  16470  frgpnabllem1  18985  pcoass  23620  dvradcnv  25001  efhalfpi  25049  sinq34lt0t  25087  efifo  25123  logm1  25164  argimgt0  25187  ang180lem4  25382  1cubr  25412  asin1  25464  atanlogsublem  25485  dvatan  25505  log2ublem3  25518  log2ub  25519  basellem9  25658  cht2  25741  log2sumbnd  26112  ax5seglem7  26713  ex-fac  28222  dp20h  30548  dpmul4  30583  hgt750lem2  31916  sqn5i  39162  decpmul  39165  sqdeccom12  39166  sq3deccom12  39167  ex-decpmul  39169  fltnltalem  39265  dirkertrigeqlem1  42374  dirkertrigeqlem3  42376  fourierdlem103  42485  sqwvfoura  42504  sqwvfourb  42505  fouriersw  42507  fmtno5lem1  43706  fmtno5lem2  43707  fmtno5lem4  43709  fmtno4prmfac  43725  fmtno5faclem2  43733  fmtno5faclem3  43734  fmtno5fac  43735  139prmALT  43750  127prm  43754  2exp11  43756  2exp340mod341  43889  nfermltl8rev  43898