Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addid1d | GIF version |
Description: 0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
addid1d | ⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addid1 7151 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝐴 + 0) = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1243 ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 0cc0 6889 + caddc 6892 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-0id 6992 |
This theorem is referenced by: subsub2 7239 negsub 7259 ltaddpos 7447 addge01 7467 add20 7469 apreap 7578 nnge1 7937 nnnn0addcl 8212 un0addcl 8215 peano2z 8281 zaddcl 8285 uzaddcl 8529 fzosubel3 9052 expadd 9297 reim0b 9462 rereb 9463 immul2 9480 resqrexlemcalc3 9614 resqrexlemnm 9616 |
Copyright terms: Public domain | W3C validator |