![]() |
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 7938 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1238 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-addass 7910 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: readdcan 8093 muladd11r 8109 cnegexlem1 8128 cnegex 8131 addcan 8133 addcan2 8134 negeu 8144 addsubass 8163 nppcan3 8177 muladd 8337 ltadd2 8372 add1p1 9164 div4p1lem1div2 9168 peano2z 9285 zaddcllempos 9286 zpnn0elfzo1 10203 exbtwnzlemstep 10243 rebtwn2zlemstep 10248 flhalf 10297 flqdiv 10316 binom2 10626 binom3 10632 bernneq 10635 omgadd 10775 cvg1nlemres 10987 recvguniqlem 10996 resqrexlemover 11012 bdtrilem 11240 bdtri 11241 bcxmas 11490 efsep 11692 efi4p 11718 efival 11733 divalglemnqt 11917 flodddiv4 11931 gcdaddm 11977 limcimolemlt 14004 tangtx 14130 binom4 14268 |
Copyright terms: Public domain | W3C validator |