Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addass | Unicode version |
Description: Alias for ax-addass 7834, for naming consistency with addassi 7886. (Contributed by NM, 10-Mar-2008.) |
Ref | Expression |
---|---|
addass |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-addass 7834 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 963 wceq 1335 wcel 2128 (class class class)co 5824 cc 7730 caddc 7735 |
This theorem was proved from axioms: ax-addass 7834 |
This theorem is referenced by: addassi 7886 addassd 7900 add12 8033 add32 8034 add32r 8035 add4 8036 nnaddcl 8853 uzaddcl 9497 xaddass 9773 fztp 9980 ser3add 10404 expadd 10461 bernneq 10538 faclbnd6 10618 resqrexlemover 10910 clim2ser 11234 clim2ser2 11235 summodclem3 11277 isumsplit 11388 cvgratnnlemseq 11423 odd2np1lem 11763 ptolemy 13156 |
Copyright terms: Public domain | W3C validator |