Metamath Proof Explorer


Theorem mulscomd

Description: Surreal multiplication commutes. Part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 6-Mar-2025)

Ref Expression
Hypotheses mulscomd.1 φ A No
mulscomd.2 φ B No
Assertion mulscomd φ A s B = B s A

Proof

Step Hyp Ref Expression
1 mulscomd.1 φ A No
2 mulscomd.2 φ B No
3 mulscom A No B No A s B = B s A
4 1 2 3 syl2anc φ A s B = B s A