Metamath Proof Explorer


Theorem negscld

Description: The surreals are closed under negation. Theorem 6(ii) of Conway p. 18. (Contributed by Scott Fenton, 3-Feb-2025)

Ref Expression
Hypothesis negscld.1 φ A No
Assertion negscld φ + s A No

Proof

Step Hyp Ref Expression
1 negscld.1 φ A No
2 negscl A No + s A No
3 1 2 syl φ + s A No