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 7874 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1227 | 1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 ∈ wcel 2135 (class class class)co 5836 ℂcc 7742 + caddc 7747 |
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 7846 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: readdcan 8029 muladd11r 8045 cnegexlem1 8064 cnegex 8067 addcan 8069 addcan2 8070 negeu 8080 addsubass 8099 nppcan3 8113 muladd 8273 ltadd2 8308 add1p1 9097 div4p1lem1div2 9101 peano2z 9218 zaddcllempos 9219 zpnn0elfzo1 10133 exbtwnzlemstep 10173 rebtwn2zlemstep 10178 flhalf 10227 flqdiv 10246 binom2 10555 binom3 10561 bernneq 10564 omgadd 10704 cvg1nlemres 10913 recvguniqlem 10922 resqrexlemover 10938 bdtrilem 11166 bdtri 11167 bcxmas 11416 efsep 11618 efi4p 11644 efival 11659 divalglemnqt 11842 flodddiv4 11856 gcdaddm 11902 limcimolemlt 13180 tangtx 13306 binom4 13444 |
Copyright terms: Public domain | W3C validator |