![]() |
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 7595 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1299 ∈ wcel 1448 (class class class)co 5706 ℂcc 7498 + caddc 7503 |
This theorem was proved from axioms: ax-addcom 7595 |
This theorem is referenced by: addid2 7772 readdcan 7773 addcomi 7777 addcomd 7784 add12 7791 add32 7792 add42 7795 cnegexlem1 7808 cnegexlem3 7810 cnegex2 7812 subsub23 7838 pncan2 7840 addsub 7844 addsub12 7846 addsubeq4 7848 sub32 7867 pnpcan2 7873 ppncan 7875 sub4 7878 negsubdi2 7892 ltadd2 8048 ltaddnegr 8054 ltaddsub2 8066 leaddsub2 8068 leltadd 8076 ltaddpos2 8082 addge02 8102 conjmulap 8350 recreclt 8516 avgle1 8812 avgle2 8813 nn0nnaddcl 8860 xaddcom 9485 fzen 9664 fzshftral 9729 flqzadd 9912 addmodidr 9987 nn0ennn 10047 ser3add 10119 bernneq2 10254 shftval2 10439 shftval4 10441 crim 10471 resqrexlemover 10622 climshft2 10914 summodclem3 10988 binom1dif 11095 isumshft 11098 arisum 11106 mertenslemi1 11143 addcos 11251 demoivreALT 11277 dvdsaddr 11332 divalgb 11417 hashdvds 11689 ioo2bl 12462 |
Copyright terms: Public domain | W3C validator |