![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addassd | GIF version |
Description: Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
addcld.1 | ⊢ (𝜑 → 𝐴 ∈ ℂ) |
addcld.2 | ⊢ (𝜑 → 𝐵 ∈ ℂ) |
addassd.3 | ⊢ (𝜑 → 𝐶 ∈ ℂ) |
Ref | Expression |
---|---|
addassd | ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | addcld.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℂ) | |
2 | addcld.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℂ) | |
3 | addassd.3 | . 2 ⊢ (𝜑 → 𝐶 ∈ ℂ) | |
4 | addass 7972 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1249 | 1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 ∈ wcel 2160 (class class class)co 5897 ℂcc 7840 + caddc 7845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-addass 7944 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: readdcan 8128 muladd11r 8144 cnegexlem1 8163 cnegex 8166 addcan 8168 addcan2 8169 negeu 8179 addsubass 8198 nppcan3 8212 muladd 8372 ltadd2 8407 add1p1 9199 div4p1lem1div2 9203 peano2z 9320 zaddcllempos 9321 zpnn0elfzo1 10240 exbtwnzlemstep 10280 rebtwn2zlemstep 10285 flhalf 10335 flqdiv 10354 binom2 10666 binom3 10672 bernneq 10675 omgadd 10817 cvg1nlemres 11029 recvguniqlem 11038 resqrexlemover 11054 bdtrilem 11282 bdtri 11283 bcxmas 11532 efsep 11734 efi4p 11760 efival 11775 divalglemnqt 11960 flodddiv4 11974 gcdaddm 12020 pcadd2 12376 4sqlem11 12436 limcimolemlt 14610 tangtx 14736 binom4 14874 |
Copyright terms: Public domain | W3C validator |