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

Theorem addid1d 7934
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 7923 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 14 1 (𝜑 → (𝐴 + 0) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1332  wcel 1481  (class class class)co 5781  cc 7641  0cc0 7643   + caddc 7646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 7751
This theorem is referenced by:  subsub2  8013  negsub  8033  ltaddneg  8209  ltaddpos  8237  addge01  8257  add20  8259  apreap  8372  nnge1  8766  nnnn0addcl  9030  un0addcl  9033  peano2z  9113  zaddcl  9117  uzaddcl  9407  xaddid1  9674  fzosubel3  10003  expadd  10365  faclbnd6  10521  omgadd  10579  reim0b  10665  rereb  10666  immul2  10683  resqrexlemcalc3  10819  resqrexlemnm  10821  max0addsup  11022  fsumsplit  11207  sumsplitdc  11232  bezoutlema  11721  cosmpi  12943  sinppi  12944  sinhalfpip  12947  trilpolemlt1  13407
  Copyright terms: Public domain W3C validator