Theorem addridd 11346

Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
muld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
addridd	⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Proof of Theorem addridd

Step	Hyp	Ref	Expression
1		muld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addrid 11326	. 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 + 0) = 𝐴)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036  0cc0 11038   + caddc 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5308  ax-pr 5376  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6455  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7370  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-ltxr 11184

This theorem is referenced by:  ltaddneg  11362  subsub2  11422  negsub  11442  ltaddpos  11640  addge01  11660  add20  11662  nnge1  12205  nnnn0addcl  12467  un0addcl  12470  uzaddcl  12854  xaddrid  13193  fzosubel3  13681  expadd  14066  faclbnd4lem4  14258  faclbnd6  14261  hashgadd  14339  ccatrid  14550  pfxmpt  14641  pfxfv  14645  pfxswrd  14668  pfxccatin12lem1  14690  pfxccatin12lem2  14693  swrdccat3blem  14701  cshweqrep  14783  relexpaddg  15015  reim0b  15081  rereb  15082  immul2  15099  max0add  15272  iseraltlem2  15645  fsumsplit  15703  sumsplit  15730  binomfallfaclem2  16005  pwp1fsum  16360  bitsinv1lem  16410  sadadd2lem2  16419  sadcaddlem  16426  bezoutlem1  16508  pcadd  16860  pcadd2  16861  pcmpt  16863  vdwapun  16945  vdwlem1  16952  chnccat  18592  mulgnn0dir  19080  psgnunilem2  19470  sylow1lem1  19573  efginvrel2  19702  efgredleme  19718  efgcpbllemb  19730  frgpnabllem1  19848  regsumfsum  21415  pzriprnglem10  21470  regsumsupp  21602  mplcoe5  22018  psdmul  22132  xrsxmet  24775  reparphti  24964  cphpyth  25183  minveclem6  25401  ovolunnul  25467  voliunlem3  25519  ovolioo  25535  itg2splitlem  25715  itg2split  25716  itgrevallem1  25762  itgsplitioo  25805  ditgsplit  25828  dvnadd  25896  dvlipcn  25961  ply1divex  26102  dvntaylp  26336  ulmshft  26355  abelthlem6  26401  cosmpi  26452  sinppi  26453  sinhalfpip  26456  logrnaddcl  26538  affineequiv  26787  chordthmlem3  26798  atanlogaddlem  26877  atanlogsublem  26879  leibpi  26906  scvxcvx  26949  dmgmn0  26989  lgamgulmlem2  26993  lgambdd  27000  logexprlim  27188  2sqblem  27394  2sq2  27396  2sqnn  27402  dchrvmasum2if  27460  dchrvmasumlem  27486  axcontlem8  29040  elntg2  29054  crctcshlem4  29888  eupth2lem3lem6  30303  ipidsq  30781  minvecolem6  30953  normpyc  31217  pjspansn  31648  lnfnmuli  32115  hstoh  32303  indsumin  32921  archirngz  33250  constrrtlc2  33877  constrsslem  33885  2sqr3minply  33924  cos9thpiminply  33932  esumpfinvallem  34218  signsvtp  34727  signlem0  34731  fsum2dsub  34751  cvxpconn  35424  cvxsconn  35425  elmrsubrn  35702  faclim2  35930  fwddifn0  36346  fwddifnp1  36347  dnizeq0  36735  knoppndvlem6  36777  bj-bary1lem  37624  poimirlem1  37942  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem11  37952  poimirlem12  37953  poimirlem17  37958  poimirlem20  37961  poimirlem22  37963  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  mblfinlem2  37979  mbfposadd  37988  itg2addnc  37995  itgaddnclem2  38000  ftc1anclem5  38018  ftc1anclem8  38021  areacirc  38034  lcmineqlem4  42471  lcmineqlem18  42485  aks4d1p1p7  42513  aks4d1p3  42517  posbezout  42539  primrootspoweq0  42545  sticksstones10  42594  sticksstones12a  42596  unitscyglem5  42638  3cubeslem2  43117  3cubeslem3r  43119  pell1qrgaplem  43301  jm2.19lem3  43419  jm2.25  43427  relexpaddss  44145  int-add01d  44611  binomcxplemnn0  44776  fperiodmullem  45736  xralrple3  45803  sumnnodd  46060  fprodaddrecnncnvlem  46337  ioodvbdlimc1lem2  46360  volioc  46400  volico  46411  stoweidlem11  46439  stoweidlem26  46454  stirlinglem12  46513  fourierdlem4  46539  fourierdlem42  46577  fourierdlem60  46594  fourierdlem61  46595  fourierdlem92  46626  fourierdlem107  46641  fouriersw  46659  etransclem24  46686  etransclem35  46697  hoidmvlelem2  47024  hspmbllem1  47054  sharhght  47293  deccarry  47753  flmrecm1  47785  nn0mnd  48649  altgsumbcALT  48823  itcovalpclem1  49140  eenglngeehlnmlem2  49208  line2y  49225  itschlc0xyqsol1  49236  itschlc0xyqsol  49237  2itscp  49251