Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addcom | GIF version |
Description: Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.) |
Ref | Expression |
---|---|
addcom | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addcom 6984 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 = wceq 1243 ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 + caddc 6892 |
This theorem was proved from axioms: ax-addcom 6984 |
This theorem is referenced by: addid2 7152 readdcan 7153 addcomi 7157 addcomd 7164 add12 7169 add32 7170 add42 7173 cnegexlem1 7186 cnegexlem3 7188 cnegex2 7190 subsub23 7216 pncan2 7218 addsub 7222 addsub12 7224 addsubeq4 7226 sub32 7245 pnpcan2 7251 ppncan 7253 sub4 7256 negsubdi2 7270 ltadd2 7416 ltaddsub2 7432 leaddsub2 7434 leltadd 7442 ltaddpos2 7448 addge02 7468 conjmulap 7705 recreclt 7866 avgle1 8165 avgle2 8166 nn0nnaddcl 8213 fzen 8907 fzshftral 8970 flqzadd 9140 nn0ennn 9209 iseradd 9243 bernneq2 9370 shftval2 9427 shftval4 9429 crim 9458 resqrexlemover 9608 climshft2 9827 |
Copyright terms: Public domain | W3C validator |