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 7718 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | mp3an 1300 | 1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)) |
Colors of variables: wff set class |
Syntax hints: = wceq 1316 ∈ wcel 1465 (class class class)co 5742 ℂcc 7586 + caddc 7591 |
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 7690 |
This theorem depends on definitions: df-bi 116 df-3an 949 |
This theorem is referenced by: 2p2e4 8815 3p2e5 8829 3p3e6 8830 4p2e6 8831 4p3e7 8832 4p4e8 8833 5p2e7 8834 5p3e8 8835 5p4e9 8836 6p2e8 8837 6p3e9 8838 7p2e9 8839 numsuc 9163 nummac 9194 numaddc 9197 6p5lem 9219 5p5e10 9220 6p4e10 9221 7p3e10 9224 8p2e10 9229 binom2i 10369 resqrexlemover 10750 3dvdsdec 11489 3dvds2dec 11490 |
Copyright terms: Public domain | W3C validator |