Theorem addlidi 11440

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7426  ℂcc 11144  0cc0 11146   + caddc 11149

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 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-resscn 11203  ax-1cn 11204  ax-icn 11205  ax-addcl 11206  ax-addrcl 11207  ax-mulcl 11208  ax-mulrcl 11209  ax-mulcom 11210  ax-addass 11211  ax-mulass 11212  ax-distr 11213  ax-i2m1 11214  ax-1ne0 11215  ax-1rid 11216  ax-rnegex 11217  ax-rrecex 11218  ax-cnre 11219  ax-pre-lttri 11220  ax-pre-lttrn 11221  ax-pre-ltadd 11222

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-po 5594  df-so 5595  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-ov 7429  df-er 8731  df-en 8971  df-dom 8972  df-sdom 8973  df-pnf 11288  df-mnf 11289  df-ltxr 11291

This theorem is referenced by:  ine0  11687  muleqadd  11896  inelr  12240  nnne0  12284  0p1e1  12372  num0h  12727  nummul1c  12764  decrmac  12773  fz0tp  13642  fz0to4untppr  13644  fzo0to3tp  13758  cats1fvn  14849  rei  15143  imi  15144  ef01bndlem  16168  gcdaddmlem  16506  dec5dvds2  17041  2exp11  17066  2exp16  17067  43prm  17098  83prm  17099  139prm  17100  163prm  17101  317prm  17102  631prm  17103  1259lem1  17107  1259lem2  17108  1259lem3  17109  1259lem4  17110  1259lem5  17111  2503lem1  17113  2503lem2  17114  2503lem3  17115  2503prm  17116  4001lem1  17117  4001lem2  17118  4001lem3  17119  4001prm  17121  frgpnabllem1  19835  pcoass  24971  dvradcnv  26377  efhalfpi  26426  sinq34lt0t  26464  efifo  26501  logm1  26543  argimgt0  26566  ang180lem4  26764  1cubr  26794  asin1  26846  atanlogsublem  26867  dvatan  26887  log2ublem3  26900  log2ub  26901  basellem9  27041  cht2  27124  log2sumbnd  27497  ax5seglem7  28766  ex-fac  30281  dp20h  32623  dpmul4  32658  hgt750lem2  34317  12gcd5e1  41506  3exp7  41556  3lexlogpow5ineq1  41557  3lexlogpow5ineq5  41563  aks4d1p1  41579  posbezout  41603  sqn5i  41890  decpmul  41893  sqdeccom12  41894  sq3deccom12  41895  ex-decpmul  41899  fltnltalem  42117  dirkertrigeqlem1  45515  dirkertrigeqlem3  45517  fourierdlem103  45626  sqwvfoura  45645  sqwvfourb  45646  fouriersw  45648  fmtno5lem1  46922  fmtno5lem2  46923  fmtno5lem4  46925  fmtno4prmfac  46941  fmtno5faclem2  46949  fmtno5faclem3  46950  fmtno5fac  46951  139prmALT  46965  127prm  46968  2exp340mod341  47102  nfermltl8rev  47111  ackval1012  47841  ackval2012  47842  ackval3012  47843