Metamath Proof Explorer


Theorem addsdid

Description: Distributive law for surreal numbers. Commuted form of part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 9-Mar-2025)

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

Proof

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