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 7864 | . 2 | |
5 | 1, 2, 3, 4 | mp3an 1319 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1335 wcel 2128 (class class class)co 5826 cc 7732 caddc 7737 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-addass 7836 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: 2p2e4 8965 3p2e5 8979 3p3e6 8980 4p2e6 8981 4p3e7 8982 4p4e8 8983 5p2e7 8984 5p3e8 8985 5p4e9 8986 6p2e8 8987 6p3e9 8988 7p2e9 8989 numsuc 9313 nummac 9344 numaddc 9347 6p5lem 9369 5p5e10 9370 6p4e10 9371 7p3e10 9374 8p2e10 9379 binom2i 10536 resqrexlemover 10921 3dvdsdec 11768 3dvds2dec 11769 |
Copyright terms: Public domain | W3C validator |