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 7011 | . 2 | |
5 | 1, 2, 3, 4 | syl3anc 1135 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1243 wcel 1393 (class class class)co 5512 cc 6887 caddc 6892 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-addass 6986 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: readdcan 7153 cnegexlem1 7186 cnegex 7189 addcan 7191 addcan2 7192 negeu 7202 addsubass 7221 nppcan3 7235 muladd 7381 ltadd2 7416 add1p1 8174 div4p1lem1div2 8177 peano2z 8281 zaddcllempos 8282 zpnn0elfzo1 9064 qbtwnzlemstep 9103 rebtwn2zlemstep 9107 flhalf 9144 flqdiv 9163 binom2 9362 binom3 9366 bernneq 9369 cvg1nlemres 9584 recvguniqlem 9592 resqrexlemover 9608 |
Copyright terms: Public domain | W3C validator |