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 7844 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1342 ∈ wcel 2135 (class class class)co 5836 ℂcc 7742 + caddc 7747 |
This theorem was proved from axioms: ax-addcom 7844 |
This theorem is referenced by: addid2 8028 readdcan 8029 addcomi 8033 addcomd 8040 add12 8047 add32 8048 add42 8051 cnegexlem1 8064 cnegexlem3 8066 cnegex2 8068 subsub23 8094 pncan2 8096 addsub 8100 addsub12 8102 addsubeq4 8104 sub32 8123 pnpcan2 8129 ppncan 8131 sub4 8134 negsubdi2 8148 ltadd2 8308 ltaddnegr 8314 ltaddsub2 8326 leaddsub2 8328 leltadd 8336 ltaddpos2 8342 addge02 8362 conjmulap 8616 recreclt 8786 avgle1 9088 avgle2 9089 nn0nnaddcl 9136 xaddcom 9788 fzen 9968 fzshftral 10033 flqzadd 10223 addmodidr 10298 nn0ennn 10358 ser3add 10430 bernneq2 10565 shftval2 10754 shftval4 10756 crim 10786 resqrexlemover 10938 climshft2 11233 summodclem3 11307 binom1dif 11414 isumshft 11417 arisum 11425 mertenslemi1 11462 addcos 11673 demoivreALT 11700 dvdsaddr 11762 divalgb 11847 hashdvds 12132 pythagtriplem2 12177 ioo2bl 13090 reeff1olem 13239 ptolemy 13292 |
Copyright terms: Public domain | W3C validator |