Theorem add-assoc

• Type: An axiom
• Validity: The proof is valid.
• Features: s, ls,
• Comment:
• Used by: add-in, add-less, double-neg, eq, eqint-neg, eqnum-add1, eqnum-add2, eqnum-addboth1, eqnum-addboth2, ex-ls-add, ex-oddeven, inv-add, ls, ls-02, ls-03, ls-zero, lsls-add-noteq, lsls-add-notgr, lsnum-add1, lsnum-add2, lsnum-add3, lsnum-add4, lsnum-addboth1, lsnum-addboth2, lst, lst-01, lst-02, lst-03, lst-04, lst-05, mone, mone-02, mone-03, neg-01, neg-02, neg-05, neg-08, neg-09, neg-10, neg-12, neg-14, neg-add, neg-zero, negadd, negadd-eq, negeq, negl-ls, negladd-ls, negr-ls, negradd-ls, neq, neq-01, nls, not-zero-pos, pls, pls-01, pls-02, pls-03, pls-04, plst, plst-01, sub-eq, sub-eq-01, sub-ls-02, ttwo, zero, zero-01, zero-02, zero-03, zero-05, zero-06, zero-07,
• Used by units in proved state: real-limit, real-multdiv, real-min-max, real-abs, real-floor-ceil, real-supinf,
• Proof exists?: No