![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addid2i | GIF version |
Description: 0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.) |
Ref | Expression |
---|---|
mul.1 | ⊢ 𝐴 ∈ ℂ |
Ref | Expression |
---|---|
addid2i | ⊢ (0 + 𝐴) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mul.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | addid2 7818 | . 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (0 + 𝐴) = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1312 ∈ wcel 1461 (class class class)co 5726 ℂcc 7539 0cc0 7541 + caddc 7544 |
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 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-17 1487 ax-ial 1495 ax-ext 2095 ax-1cn 7632 ax-icn 7634 ax-addcl 7635 ax-mulcl 7637 ax-addcom 7639 ax-i2m1 7644 ax-0id 7647 |
This theorem depends on definitions: df-bi 116 df-cleq 2106 df-clel 2109 |
This theorem is referenced by: ine0 8069 inelr 8258 muleqadd 8336 0p1e1 8738 iap0 8841 num0h 9091 nummul1c 9128 decrmac 9137 decmul1 9143 fz0tp 9788 fzo0to3tp 9883 rei 10558 imi 10559 resqrexlemover 10668 ef01bndlem 11308 ex-fac 12624 |
Copyright terms: Public domain | W3C validator |