![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addid2d | GIF version |
Description: 0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
Ref | Expression |
---|---|
addid2d | ⊢ (𝜑 → (0 + 𝐴) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addid2 7684 | . 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (0 + 𝐴) = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1290 ∈ wcel 1439 (class class class)co 5668 ℂcc 7411 0cc0 7413 + caddc 7416 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 ax-ext 2071 ax-1cn 7501 ax-icn 7503 ax-addcl 7504 ax-mulcl 7506 ax-addcom 7508 ax-i2m1 7513 ax-0id 7516 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 df-clel 2085 |
This theorem is referenced by: negeu 7736 ltadd2 7960 subge0 8016 sublt0d 8110 un0addcl 8769 lincmb01cmp 9483 modsumfzodifsn 9866 rennim 10498 max0addsup 10715 fsumsplit 10864 sumsplitdc 10889 fisum0diag2 10904 isumsplit 10948 arisum2 10956 efaddlem 11027 eftlub 11043 ef4p 11047 moddvds 11146 gcdaddm 11316 bezoutlemb 11330 |
Copyright terms: Public domain | W3C validator |