Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addassd | Unicode 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 7904 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1233 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1348 wcel 2141 (class class class)co 5853 cc 7772 caddc 7777 |
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 7876 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: readdcan 8059 muladd11r 8075 cnegexlem1 8094 cnegex 8097 addcan 8099 addcan2 8100 negeu 8110 addsubass 8129 nppcan3 8143 muladd 8303 ltadd2 8338 add1p1 9127 div4p1lem1div2 9131 peano2z 9248 zaddcllempos 9249 zpnn0elfzo1 10164 exbtwnzlemstep 10204 rebtwn2zlemstep 10209 flhalf 10258 flqdiv 10277 binom2 10587 binom3 10593 bernneq 10596 omgadd 10737 cvg1nlemres 10949 recvguniqlem 10958 resqrexlemover 10974 bdtrilem 11202 bdtri 11203 bcxmas 11452 efsep 11654 efi4p 11680 efival 11695 divalglemnqt 11879 flodddiv4 11893 gcdaddm 11939 limcimolemlt 13427 tangtx 13553 binom4 13691 |
Copyright terms: Public domain | W3C validator |