Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addassi | GIF version |
Description: Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 | ⊢ 𝐴 ∈ ℂ |
axi.2 | ⊢ 𝐵 ∈ ℂ |
axi.3 | ⊢ 𝐶 ∈ ℂ |
Ref | Expression |
---|---|
addassi | ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 | . 2 ⊢ 𝐴 ∈ ℂ | |
2 | axi.2 | . 2 ⊢ 𝐵 ∈ ℂ | |
3 | axi.3 | . 2 ⊢ 𝐶 ∈ ℂ | |
4 | addass 7862 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1319 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff set class |
Syntax hints: = wceq 1335 ∈ wcel 2128 (class class class)co 5824 ℂcc 7730 + caddc 7735 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-addass 7834 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 2p2e4 8960 3p2e5 8974 3p3e6 8975 4p2e6 8976 4p3e7 8977 4p4e8 8978 5p2e7 8979 5p3e8 8980 5p4e9 8981 6p2e8 8982 6p3e9 8983 7p2e9 8984 numsuc 9308 nummac 9339 numaddc 9342 6p5lem 9364 5p5e10 9365 6p4e10 9366 7p3e10 9369 8p2e10 9374 binom2i 10527 resqrexlemover 10910 3dvdsdec 11756 3dvds2dec 11757 |
Copyright terms: Public domain | W3C validator |