Theorem mulslidd

Description: Surreal one is a left identity element for multiplication. (Contributed by Scott Fenton, 14-Mar-2025)

	Ref	Expression
Hypothesis	mulslidd.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	mulslidd	$$⊢\phi \to 1_s{\cdot }_{s}A=A$$

Proof

Step	Hyp	Ref	Expression
1		mulslidd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		mulslid	$$⊢A\in \mathrm{No}\to 1_s{\cdot }_{s}A=A$$
3	1 2	syl	$$⊢\phi \to 1_s{\cdot }_{s}A=A$$