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 7750 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1216 | 1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 ∈ wcel 1480 (class class class)co 5774 ℂcc 7618 + caddc 7623 |
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 7722 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: readdcan 7902 muladd11r 7918 cnegexlem1 7937 cnegex 7940 addcan 7942 addcan2 7943 negeu 7953 addsubass 7972 nppcan3 7986 muladd 8146 ltadd2 8181 add1p1 8969 div4p1lem1div2 8973 peano2z 9090 zaddcllempos 9091 zpnn0elfzo1 9985 exbtwnzlemstep 10025 rebtwn2zlemstep 10030 flhalf 10075 flqdiv 10094 binom2 10403 binom3 10409 bernneq 10412 omgadd 10548 cvg1nlemres 10757 recvguniqlem 10766 resqrexlemover 10782 bdtrilem 11010 bdtri 11011 bcxmas 11258 efsep 11397 efi4p 11424 efival 11439 divalglemnqt 11617 flodddiv4 11631 gcdaddm 11672 limcimolemlt 12802 tangtx 12919 |
Copyright terms: Public domain | W3C validator |