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 7743 | . 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 5767 cc 7611 caddc 7616 |
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 7715 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: readdcan 7895 muladd11r 7911 cnegexlem1 7930 cnegex 7933 addcan 7935 addcan2 7936 negeu 7946 addsubass 7965 nppcan3 7979 muladd 8139 ltadd2 8174 add1p1 8962 div4p1lem1div2 8966 peano2z 9083 zaddcllempos 9084 zpnn0elfzo1 9978 exbtwnzlemstep 10018 rebtwn2zlemstep 10023 flhalf 10068 flqdiv 10087 binom2 10396 binom3 10402 bernneq 10405 omgadd 10541 cvg1nlemres 10750 recvguniqlem 10759 resqrexlemover 10775 bdtrilem 11003 bdtri 11004 bcxmas 11251 efsep 11386 efi4p 11413 efival 11428 divalglemnqt 11606 flodddiv4 11620 gcdaddm 11661 limcimolemlt 12791 tangtx 12908 |
Copyright terms: Public domain | W3C validator |