Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addass | GIF version |
Description: Alias for ax-addass 6986, for naming consistency with addassi 7035. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addass 6986 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ w3a 885 = wceq 1243 ∈ wcel 1393 (class class class)co 5512 ℂcc 6887 + caddc 6892 |
This theorem was proved from axioms: ax-addass 6986 |
This theorem is referenced by: addassi 7035 addassd 7049 add12 7169 add32 7170 add32r 7171 add4 7172 nnaddcl 7934 uzaddcl 8529 fztp 8940 iseradd 9243 expadd 9297 bernneq 9369 resqrexlemover 9608 clim2iser 9857 clim2iser2 9858 |
Copyright terms: Public domain | W3C validator |