Metamath Proof Explorer

Theorem mulsassd

Description: Associative law for surreal multiplication. Part of theorem 7 of Conway p. 19. (Contributed by Scott Fenton, 10-Mar-2025)

Ref Expression
Hypotheses mulsassd.1 ⊢ φ → A ∈ No
mulsassd.2 ⊢ φ → B ∈ No
mulsassd.3 ⊢ φ → C ∈ No
Assertion mulsassd ⊢ φ → A ⋅ s B ⋅ s C = A ⋅ s B ⋅ s C

Proof

Step Hyp Ref Expression
1 mulsassd.1 ⊢ φ → A ∈ No
2 mulsassd.2 ⊢ φ → B ∈ No
3 mulsassd.3 ⊢ φ → C ∈ No
4 mulsass ⊢ 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