Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addid2 | GIF version |
Description: 0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.) |
Ref | Expression |
---|---|
addid2 | ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0cn 7751 | . . 3 ⊢ 0 ∈ ℂ | |
2 | addcom 7892 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴)) | |
3 | 1, 2 | mpan2 421 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴)) |
4 | addid1 7893 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | |
5 | 3, 4 | eqtr3d 2172 | 1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ∈ wcel 1480 (class class class)co 5767 ℂcc 7611 0cc0 7613 + caddc 7616 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2119 ax-1cn 7706 ax-icn 7708 ax-addcl 7709 ax-mulcl 7711 ax-addcom 7713 ax-i2m1 7718 ax-0id 7721 |
This theorem depends on definitions: df-bi 116 df-cleq 2130 df-clel 2133 |
This theorem is referenced by: readdcan 7895 addid2i 7898 addid2d 7905 cnegexlem1 7930 cnegexlem2 7931 addcan 7935 negneg 8005 fzoaddel2 9963 divfl0 10062 modqid 10115 sumrbdclem 11138 summodclem2a 11143 fisum0diag2 11209 eftlub 11385 gcdid 11663 ptolemy 12894 |
Copyright terms: Public domain | W3C validator |