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 7720 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1331 ∈ wcel 1480 (class class class)co 5774 ℂcc 7618 + caddc 7623 |
This theorem was proved from axioms: ax-addcom 7720 |
This theorem is referenced by: addid2 7901 readdcan 7902 addcomi 7906 addcomd 7913 add12 7920 add32 7921 add42 7924 cnegexlem1 7937 cnegexlem3 7939 cnegex2 7941 subsub23 7967 pncan2 7969 addsub 7973 addsub12 7975 addsubeq4 7977 sub32 7996 pnpcan2 8002 ppncan 8004 sub4 8007 negsubdi2 8021 ltadd2 8181 ltaddnegr 8187 ltaddsub2 8199 leaddsub2 8201 leltadd 8209 ltaddpos2 8215 addge02 8235 conjmulap 8489 recreclt 8658 avgle1 8960 avgle2 8961 nn0nnaddcl 9008 xaddcom 9644 fzen 9823 fzshftral 9888 flqzadd 10071 addmodidr 10146 nn0ennn 10206 ser3add 10278 bernneq2 10413 shftval2 10598 shftval4 10600 crim 10630 resqrexlemover 10782 climshft2 11075 summodclem3 11149 binom1dif 11256 isumshft 11259 arisum 11267 mertenslemi1 11304 addcos 11453 demoivreALT 11480 dvdsaddr 11537 divalgb 11622 hashdvds 11897 ioo2bl 12712 ptolemy 12905 |
Copyright terms: Public domain | W3C validator |