Metamath Proof Explorer


Theorem addsassd

Description: Surreal addition is associative. Part of theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 22-Jan-2025)

Ref Expression
Hypotheses addsassd.1 φ A No
addsassd.2 φ B No
addsassd.3 φ C No
Assertion addsassd φ A + s B + s C = A + s B + s C

Proof

Step Hyp Ref Expression
1 addsassd.1 φ A No
2 addsassd.2 φ B No
3 addsassd.3 φ C No
4 addsass A No B No C No A + s B + s C = A + s B + s C
5 1 2 3 4 syl3anc φ A + s B + s C = A + s B + s C