Metamath Proof Explorer


Theorem mulslidd

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

Ref Expression
Hypothesis mulslidd.1 φ A No
Assertion mulslidd φ 1 s s A = A

Proof

Step Hyp Ref Expression
1 mulslidd.1 φ A No
2 mulslid A No 1 s s A = A
3 1 2 syl φ 1 s s A = A