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

Theorem addid1d 7610
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 7599 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 14 1 (𝜑 → (𝐴 + 0) = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  wcel 1438  (class class class)co 5634  cc 7327  0cc0 7329   + caddc 7332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-0id 7432
This theorem is referenced by:  subsub2  7689  negsub  7709  ltaddneg  7881  ltaddpos  7909  addge01  7929  add20  7931  apreap  8040  nnge1  8417  nnnn0addcl  8673  un0addcl  8676  peano2z  8756  zaddcl  8760  uzaddcl  9043  fzosubel3  9572  expadd  9962  faclbnd6  10117  omgadd  10175  reim0b  10261  rereb  10262  immul2  10279  resqrexlemcalc3  10414  resqrexlemnm  10416  max0addsup  10617  fsumsplit  10764  sumsplitdc  10789  bezoutlema  11081
  Copyright terms: Public domain W3C validator