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 7864 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1220 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1335 wcel 2128 (class class class)co 5826 cc 7732 caddc 7737 |
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 7836 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: readdcan 8019 muladd11r 8035 cnegexlem1 8054 cnegex 8057 addcan 8059 addcan2 8060 negeu 8070 addsubass 8089 nppcan3 8103 muladd 8263 ltadd2 8298 add1p1 9087 div4p1lem1div2 9091 peano2z 9208 zaddcllempos 9209 zpnn0elfzo1 10116 exbtwnzlemstep 10156 rebtwn2zlemstep 10161 flhalf 10210 flqdiv 10229 binom2 10538 binom3 10544 bernneq 10547 omgadd 10687 cvg1nlemres 10896 recvguniqlem 10905 resqrexlemover 10921 bdtrilem 11149 bdtri 11150 bcxmas 11397 efsep 11599 efi4p 11625 efival 11640 divalglemnqt 11823 flodddiv4 11837 gcdaddm 11883 limcimolemlt 13103 tangtx 13229 binom4 13367 |
Copyright terms: Public domain | W3C validator |