Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addass | Unicode version |
Description: Alias for ax-addass 7876, for naming consistency with addassi 7928. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addass |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addass 7876 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 973 wceq 1348 wcel 2141 (class class class)co 5853 cc 7772 caddc 7777 |
This theorem was proved from axioms: ax-addass 7876 |
This theorem is referenced by: addassi 7928 addassd 7942 add12 8077 add32 8078 add32r 8079 add4 8080 nnaddcl 8898 uzaddcl 9545 xaddass 9826 fztp 10034 ser3add 10461 expadd 10518 bernneq 10596 faclbnd6 10678 resqrexlemover 10974 clim2ser 11300 clim2ser2 11301 summodclem3 11343 isumsplit 11454 cvgratnnlemseq 11489 odd2np1lem 11831 ptolemy 13539 |
Copyright terms: Public domain | W3C validator |