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 7883 | . . 3 ⊢ 0 ∈ ℂ | |
2 | addcom 8027 | . . 3 ⊢ ((𝐴 ∈ ℂ ∧ 0 ∈ ℂ) → (𝐴 + 0) = (0 + 𝐴)) | |
3 | 1, 2 | mpan2 422 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = (0 + 𝐴)) |
4 | addid1 8028 | . 2 ⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴) | |
5 | 3, 4 | eqtr3d 2199 | 1 ⊢ (𝐴 ∈ ℂ → (0 + 𝐴) = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 ∈ wcel 2135 (class class class)co 5837 ℂcc 7743 0cc0 7745 + caddc 7748 |
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 7838 ax-icn 7840 ax-addcl 7841 ax-mulcl 7843 ax-addcom 7845 ax-i2m1 7850 ax-0id 7853 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-clel 2160 |
This theorem is referenced by: readdcan 8030 addid2i 8033 addid2d 8040 cnegexlem1 8065 cnegexlem2 8066 addcan 8070 negneg 8140 fz0to4untppr 10050 fzoaddel2 10119 divfl0 10222 modqid 10275 sumrbdclem 11308 summodclem2a 11312 fisum0diag2 11378 eftlub 11621 gcdid 11908 ptolemy 13312 |
Copyright terms: Public domain | W3C validator |