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 7011 | . 2 | |
5 | 1, 2, 3, 4 | mp3an 1232 | 1 |
Colors of variables: wff set class |
Syntax hints: 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: 2p2e4 8037 3p2e5 8052 3p3e6 8053 4p2e6 8054 4p3e7 8055 4p4e8 8056 5p2e7 8057 5p3e8 8058 5p4e9 8059 5p5e10 8060 6p2e8 8061 6p3e9 8062 6p4e10 8063 7p2e9 8064 7p3e10 8065 8p2e10 8066 numsuc 8379 nummac 8399 numaddc 8402 6p5lem 8416 binom2i 9360 resqrexlemover 9608 |
Copyright terms: Public domain | W3C validator |