Metamath Proof Explorer


Theorem mulsridd

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

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

Proof

Step Hyp Ref Expression
1 mulsridd.1 φ A No
2 mulsrid A No A s 1 s = A
3 1 2 syl φ A s 1 s = A