Theorem addlidi 11403

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7404  ℂcc 11107  0cc0 11109   + caddc 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-po 5581  df-so 5582  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11251  df-mnf 11252  df-ltxr 11254

This theorem is referenced by:  ine0  11650  muleqadd  11859  inelr  12203  nnne0  12247  0p1e1  12335  num0h  12690  nummul1c  12727  decrmac  12736  fz0tp  13605  fz0to4untppr  13607  fzo0to3tp  13721  cats1fvn  14812  rei  15106  imi  15107  ef01bndlem  16131  gcdaddmlem  16469  dec5dvds2  17004  2exp11  17029  2exp16  17030  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem1  17070  1259lem2  17071  1259lem3  17072  1259lem4  17073  1259lem5  17074  2503lem1  17076  2503lem2  17077  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001prm  17084  frgpnabllem1  19790  pcoass  24901  dvradcnv  26307  efhalfpi  26356  sinq34lt0t  26394  efifo  26431  logm1  26473  argimgt0  26496  ang180lem4  26694  1cubr  26724  asin1  26776  atanlogsublem  26797  dvatan  26817  log2ublem3  26830  log2ub  26831  basellem9  26971  cht2  27054  log2sumbnd  27427  ax5seglem7  28696  ex-fac  30208  dp20h  32547  dpmul4  32582  hgt750lem2  34192  12gcd5e1  41383  3exp7  41433  3lexlogpow5ineq1  41434  3lexlogpow5ineq5  41440  aks4d1p1  41456  posbezout  41479  sqn5i  41737  decpmul  41740  sqdeccom12  41741  sq3deccom12  41742  ex-decpmul  41746  fltnltalem  41964  dirkertrigeqlem1  45368  dirkertrigeqlem3  45370  fourierdlem103  45479  sqwvfoura  45498  sqwvfourb  45499  fouriersw  45501  fmtno5lem1  46775  fmtno5lem2  46776  fmtno5lem4  46778  fmtno4prmfac  46794  fmtno5faclem2  46802  fmtno5faclem3  46803  fmtno5fac  46804  139prmALT  46818  127prm  46821  2exp340mod341  46955  nfermltl8rev  46964  ackval1012  47633  ackval2012  47634  ackval3012  47635