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

Theorem addid1d 7324
 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 7313 . 2 (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)
31, 2syl 14 1 (𝜑 → (𝐴 + 0) = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1285   ∈ wcel 1434  (class class class)co 5543  ℂcc 7041  0cc0 7043   + caddc 7046 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-0id 7146 This theorem is referenced by:  subsub2  7403  negsub  7423  ltaddneg  7595  ltaddpos  7623  addge01  7643  add20  7645  apreap  7754  nnge1  8129  nnnn0addcl  8385  un0addcl  8388  peano2z  8468  zaddcl  8472  uzaddcl  8755  fzosubel3  9282  expadd  9615  faclbnd6  9768  omgadd  9826  reim0b  9887  rereb  9888  immul2  9905  resqrexlemcalc3  10040  resqrexlemnm  10042  max0addsup  10243  bezoutlema  10532
 Copyright terms: Public domain W3C validator