![]() |
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 7674 | . 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) | |
5 | 1, 2, 3, 4 | syl3anc 1199 | 1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1314 ∈ wcel 1463 (class class class)co 5728 ℂcc 7545 + caddc 7550 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-addass 7647 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: readdcan 7825 muladd11r 7841 cnegexlem1 7860 cnegex 7863 addcan 7865 addcan2 7866 negeu 7876 addsubass 7895 nppcan3 7909 muladd 8065 ltadd2 8100 add1p1 8873 div4p1lem1div2 8877 peano2z 8994 zaddcllempos 8995 zpnn0elfzo1 9878 exbtwnzlemstep 9918 rebtwn2zlemstep 9923 flhalf 9968 flqdiv 9987 binom2 10296 binom3 10302 bernneq 10305 omgadd 10441 cvg1nlemres 10649 recvguniqlem 10658 resqrexlemover 10674 bdtrilem 10902 bdtri 10903 bcxmas 11150 efsep 11248 efi4p 11275 efival 11290 divalglemnqt 11465 flodddiv4 11479 gcdaddm 11520 limcimolemlt 12589 |
Copyright terms: Public domain | W3C validator |