![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addass | GIF version |
Description: Alias for ax-addass 7641, for naming consistency with addassi 7692. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addass 7641 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 943 = wceq 1312 ∈ wcel 1461 (class class class)co 5726 ℂcc 7539 + caddc 7544 |
This theorem was proved from axioms: ax-addass 7641 |
This theorem is referenced by: addassi 7692 addassd 7706 add12 7837 add32 7838 add32r 7839 add4 7840 nnaddcl 8644 uzaddcl 9277 xaddass 9539 fztp 9745 ser3add 10165 expadd 10222 bernneq 10299 faclbnd6 10377 resqrexlemover 10668 clim2ser 10992 clim2ser2 10993 summodclem3 11035 isumsplit 11146 cvgratnnlemseq 11181 odd2np1lem 11411 |
Copyright terms: Public domain | W3C validator |