![]() |
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 7913 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1353 ∈ wcel 2148 (class class class)co 5877 ℂcc 7811 + caddc 7816 |
This theorem was proved from axioms: ax-addcom 7913 |
This theorem is referenced by: addlid 8098 readdcan 8099 addcomi 8103 addcomd 8110 add12 8117 add32 8118 add42 8121 cnegexlem1 8134 cnegexlem3 8136 cnegex2 8138 subsub23 8164 pncan2 8166 addsub 8170 addsub12 8172 addsubeq4 8174 sub32 8193 pnpcan2 8199 ppncan 8201 sub4 8204 negsubdi2 8218 ltadd2 8378 ltaddnegr 8384 ltaddsub2 8396 leaddsub2 8398 leltadd 8406 ltaddpos2 8412 addge02 8432 conjmulap 8688 recreclt 8859 avgle1 9161 avgle2 9162 nn0nnaddcl 9209 xaddcom 9863 fzen 10045 fzshftral 10110 flqzadd 10300 addmodidr 10375 nn0ennn 10435 ser3add 10507 bernneq2 10644 shftval2 10837 shftval4 10839 crim 10869 resqrexlemover 11021 climshft2 11316 summodclem3 11390 binom1dif 11497 isumshft 11500 arisum 11508 mertenslemi1 11545 addcos 11756 demoivreALT 11783 dvdsaddr 11846 divalgb 11932 hashdvds 12223 pythagtriplem2 12268 mulgnndir 13017 cncrng 13548 ioo2bl 14128 reeff1olem 14277 ptolemy 14330 |
Copyright terms: Public domain | W3C validator |