![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addassi | Unicode version |
Description: Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Ref | Expression |
---|---|
axi.1 |
![]() ![]() ![]() ![]() |
axi.2 |
![]() ![]() ![]() ![]() |
axi.3 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
addassi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | axi.2 |
. 2
![]() ![]() ![]() ![]() | |
3 | axi.3 |
. 2
![]() ![]() ![]() ![]() | |
4 | addass 7674 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | mp3an 1298 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-addass 7647 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: 2p2e4 8751 3p2e5 8765 3p3e6 8766 4p2e6 8767 4p3e7 8768 4p4e8 8769 5p2e7 8770 5p3e8 8771 5p4e9 8772 6p2e8 8773 6p3e9 8774 7p2e9 8775 numsuc 9099 nummac 9130 numaddc 9133 6p5lem 9155 5p5e10 9156 6p4e10 9157 7p3e10 9160 8p2e10 9165 binom2i 10294 resqrexlemover 10674 3dvdsdec 11410 3dvds2dec 11411 |
Copyright terms: Public domain | W3C validator |