![]() |
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 7943 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | mp3an 1337 |
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 7915 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: 2p2e4 9048 3p2e5 9062 3p3e6 9063 4p2e6 9064 4p3e7 9065 4p4e8 9066 5p2e7 9067 5p3e8 9068 5p4e9 9069 6p2e8 9070 6p3e9 9071 7p2e9 9072 numsuc 9399 nummac 9430 numaddc 9433 6p5lem 9455 5p5e10 9456 6p4e10 9457 7p3e10 9460 8p2e10 9465 binom2i 10631 resqrexlemover 11021 3dvdsdec 11872 3dvds2dec 11873 lgsdir2lem2 14515 2lgsoddprmlem3d 14543 |
Copyright terms: Public domain | W3C validator |