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	⊢ ( 𝜑 → 𝐴 ∈ No )
	mulsassd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	mulsassd.3	⊢ ( 𝜑 → 𝐶 ∈ No )
Assertion	mulsassd	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝐵 ·s 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulsassd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		mulsassd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		mulsassd.3	⊢ ( 𝜑 → 𝐶 ∈ No )
4		mulsass	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ( 𝐴 ·s 𝐵 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝐵 ·s 𝐶 ) ) )
5	1 2 3 4	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 ·s 𝐵 ) ·s 𝐶 ) = ( 𝐴 ·s ( 𝐵 ·s 𝐶 ) ) )