![]() |
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 10193, for naming consistency with addassi 10240. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addass 10193 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1072 = wceq 1632 ∈ wcel 2139 (class class class)co 6813 ℂcc 10126 + caddc 10131 |
This theorem was proved from axioms: ax-addass 10193 |
This theorem is referenced by: addassi 10240 addassd 10254 00id 10403 addid2 10411 add12 10445 add32 10446 add32r 10447 add4 10448 nnaddcl 11234 uzaddcl 11937 xaddass 12272 fztp 12590 seradd 13037 expadd 13096 bernneq 13184 faclbnd6 13280 hashgadd 13358 swrds2 13885 clim2ser 14584 clim2ser2 14585 summolem3 14644 isumsplit 14771 fsumcube 14990 odd2np1lem 15266 prmlem0 16014 cnaddablx 18471 cnaddabl 18472 zaddablx 18475 cncrng 19969 cnlmod 23140 pjthlem1 23408 ptolemy 24447 bcp1ctr 25203 cnaddabloOLD 27745 pjhthlem1 28559 dnibndlem5 32778 mblfinlem2 33760 mogoldbblem 42139 nnsgrp 42327 2zrngasgrp 42450 |
Copyright terms: Public domain | W3C validator |