![]() |
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 | addlid 8094 | . 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (0 + 𝐴) = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1353 ∈ wcel 2148 (class class class)co 5874 ℂcc 7808 0cc0 7810 + caddc 7813 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1cn 7903 ax-icn 7905 ax-addcl 7906 ax-mulcl 7908 ax-addcom 7910 ax-i2m1 7915 ax-0id 7918 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 df-clel 2173 |
This theorem is referenced by: ine0 8349 inelr 8539 muleqadd 8623 0p1e1 9031 iap0 9140 num0h 9393 nummul1c 9430 decrmac 9439 decmul1 9445 fz0tp 10119 fz0to4untppr 10121 fzo0to3tp 10216 rei 10903 imi 10904 resqrexlemover 11014 ef01bndlem 11759 efhalfpi 14113 sinq34lt0t 14145 ex-fac 14362 |
Copyright terms: Public domain | W3C validator |