| 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 11220, for naming consistency with addassi 11271. (Contributed by NM, 10-Mar-2008.) |
| Ref | Expression |
|---|---|
| addass | ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-addass 11220 | 1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 (class class class)co 7431 ℂcc 11153 + caddc 11158 |
| This theorem was proved from axioms: ax-addass 11220 |
| This theorem is referenced by: addassi 11271 addassd 11283 00id 11436 addlid 11444 add12 11479 add32 11480 add32r 11481 add4 11482 nnaddcl 12289 uzaddcl 12946 xaddass 13291 fztp 13620 seradd 14085 expadd 14145 bernneq 14268 faclbnd6 14338 hashgadd 14416 swrds2 14979 clim2ser 15691 clim2ser2 15692 summolem3 15750 isumsplit 15876 fsumcube 16096 odd2np1lem 16377 prmlem0 17143 cnaddablx 19886 cnaddabl 19887 zaddablx 19890 cncrng 21401 cncrngOLD 21402 cnlmod 25173 pjthlem1 25471 ptolemy 26538 bcp1ctr 27323 cnaddabloOLD 30600 pjhthlem1 31410 dnibndlem5 36483 mblfinlem2 37665 facp2 42144 fac2xp3 42240 2xp3dxp2ge1d 42242 factwoffsmonot 42243 mogoldbblem 47707 nnsgrp 48093 nn0mnd 48095 2zrngasgrp 48162 |
| Copyright terms: Public domain | W3C validator |