Theorem addid2i 11173

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  (class class class)co 7267  ℂcc 10879  0cc0 10881   + caddc 10884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578  ax-resscn 10938  ax-1cn 10939  ax-icn 10940  ax-addcl 10941  ax-addrcl 10942  ax-mulcl 10943  ax-mulrcl 10944  ax-mulcom 10945  ax-addass 10946  ax-mulass 10947  ax-distr 10948  ax-i2m1 10949  ax-1ne0 10950  ax-1rid 10951  ax-rnegex 10952  ax-rrecex 10953  ax-cnre 10954  ax-pre-lttri 10955  ax-pre-lttrn 10956  ax-pre-ltadd 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5074  df-opab 5136  df-mpt 5157  df-id 5484  df-po 5498  df-so 5499  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433  df-fv 6434  df-ov 7270  df-er 8485  df-en 8721  df-dom 8722  df-sdom 8723  df-pnf 11021  df-mnf 11022  df-ltxr 11024

This theorem is referenced by:  ine0  11420  muleqadd  11629  inelr  11973  nnne0  12017  0p1e1  12105  num0h  12459  nummul1c  12496  decrmac  12505  fz0tp  13367  fz0to4untppr  13369  fzo0to3tp  13483  cats1fvn  14581  rei  14877  imi  14878  ef01bndlem  15903  gcdaddmlem  16241  dec5dvds2  16776  2exp11  16801  2exp16  16802  43prm  16833  83prm  16834  139prm  16835  163prm  16836  317prm  16837  631prm  16838  1259lem1  16842  1259lem2  16843  1259lem3  16844  1259lem4  16845  1259lem5  16846  2503lem1  16848  2503lem2  16849  2503lem3  16850  2503prm  16851  4001lem1  16852  4001lem2  16853  4001lem3  16854  4001prm  16856  frgpnabllem1  19484  pcoass  24197  dvradcnv  25590  efhalfpi  25638  sinq34lt0t  25676  efifo  25713  logm1  25754  argimgt0  25777  ang180lem4  25972  1cubr  26002  asin1  26054  atanlogsublem  26075  dvatan  26095  log2ublem3  26108  log2ub  26109  basellem9  26248  cht2  26331  log2sumbnd  26702  ax5seglem7  27313  ex-fac  28823  dp20h  31161  dpmul4  31196  hgt750lem2  32640  12gcd5e1  40019  3exp7  40069  3lexlogpow5ineq1  40070  3lexlogpow5ineq5  40076  aks4d1p1  40092  sqn5i  40321  decpmul  40324  sqdeccom12  40325  sq3deccom12  40326  ex-decpmul  40328  fltnltalem  40507  dirkertrigeqlem1  43620  dirkertrigeqlem3  43622  fourierdlem103  43731  sqwvfoura  43750  sqwvfourb  43751  fouriersw  43753  fmtno5lem1  44983  fmtno5lem2  44984  fmtno5lem4  44986  fmtno4prmfac  45002  fmtno5faclem2  45010  fmtno5faclem3  45011  fmtno5fac  45012  139prmALT  45026  127prm  45029  2exp340mod341  45163  nfermltl8rev  45172  ackval1012  46014  ackval2012  46015  ackval3012  46016