Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > addass | Structured version Visualization version GIF version |
Description: Alias for ax-addass 10590, for naming consistency with addassi 10639. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addass 10590 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1079 = wceq 1528 ∈ wcel 2105 (class class class)co 7145 ℂcc 10523 + caddc 10528 |
This theorem was proved from axioms: ax-addass 10590 |
This theorem is referenced by: addassi 10639 addassd 10651 00id 10803 addid2 10811 add12 10845 add32 10846 add32r 10847 add4 10848 nnaddcl 11648 uzaddcl 12292 xaddass 12630 fztp 12951 seradd 13400 expadd 13459 bernneq 13578 faclbnd6 13647 hashgadd 13726 swrds2 14290 clim2ser 14999 clim2ser2 15000 summolem3 15059 isumsplit 15183 fsumcube 15402 odd2np1lem 15677 prmlem0 16427 cnaddablx 18917 cnaddabl 18918 zaddablx 18921 cncrng 20494 cnlmod 23671 pjthlem1 23967 ptolemy 25009 bcp1ctr 25782 cnaddabloOLD 28285 pjhthlem1 29095 dnibndlem5 33718 mblfinlem2 34811 mogoldbblem 43762 nnsgrp 43961 nn0mnd 43963 2zrngasgrp 44139 |
Copyright terms: Public domain | W3C validator |