Metamath Proof Explorer


Theorem slenegd

Description: Negative of both sides of surreal less-than or equal. (Contributed by Scott Fenton, 14-Mar-2025)

Ref Expression
Hypotheses sltnegd.1 φ A No
sltnegd.2 φ B No
Assertion slenegd φ A s B + s B s + s A

Proof

Step Hyp Ref Expression
1 sltnegd.1 φ A No
2 sltnegd.2 φ B No
3 sleneg A No B No A s B + s B s + s A
4 1 2 3 syl2anc φ A s B + s B s + s A