ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addid1d GIF version

Theorem addid1d 8068
Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1 (𝜑𝐴 ∈ ℂ)
Assertion
Ref Expression
addid1d (𝜑 → (𝐴 + 0) = 𝐴)

Proof of Theorem addid1d
StepHypRef Expression
1 muld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addid1 8057 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 14 1 (𝜑 → (𝐴 + 0) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1348  wcel 2141  (class class class)co 5853  cc 7772  0cc0 7774   + caddc 7777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 7882
This theorem is referenced by:  subsub2  8147  negsub  8167  ltaddneg  8343  ltaddpos  8371  addge01  8391  add20  8393  apreap  8506  nnge1  8901  nnnn0addcl  9165  un0addcl  9168  peano2z  9248  zaddcl  9252  uzaddcl  9545  xaddid1  9819  fzosubel3  10152  expadd  10518  faclbnd6  10678  omgadd  10737  reim0b  10826  rereb  10827  immul2  10844  resqrexlemcalc3  10980  resqrexlemnm  10982  max0addsup  11183  fsumsplit  11370  sumsplitdc  11395  bezoutlema  11954  pcadd  12293  pcmpt  12295  cosmpi  13531  sinppi  13532  sinhalfpip  13535  trilpolemlt1  14073
  Copyright terms: Public domain W3C validator