Metamath Proof Explorer
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 |
|
|
|
addsdid.2 |
|
|
|
addsdid.3 |
|
|
Assertion |
addsdid |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
addsdid.1 |
|
2 |
|
addsdid.2 |
|
3 |
|
addsdid.3 |
|
4 |
|
addsdi |
|
5 |
1 2 3 4
|
syl3anc |
|