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 8028 | . 2 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (0 + 𝐴) = 𝐴 |
Colors of variables: wff set class |
Syntax hints: = wceq 1342 ∈ wcel 2135 (class class class)co 5836 ℂcc 7742 0cc0 7744 + caddc 7747 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-ext 2146 ax-1cn 7837 ax-icn 7839 ax-addcl 7840 ax-mulcl 7842 ax-addcom 7844 ax-i2m1 7849 ax-0id 7852 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-clel 2160 |
This theorem is referenced by: ine0 8283 inelr 8473 muleqadd 8556 0p1e1 8962 iap0 9071 num0h 9324 nummul1c 9361 decrmac 9370 decmul1 9376 fz0tp 10047 fz0to4untppr 10049 fzo0to3tp 10144 rei 10827 imi 10828 resqrexlemover 10938 ef01bndlem 11683 efhalfpi 13267 sinq34lt0t 13299 ex-fac 13452 |
Copyright terms: Public domain | W3C validator |