Theorem sltaddsub2d

Description: Surreal less-than relationship between subtraction and addition. (Contributed by Scott Fenton, 28-Feb-2025)

	Ref	Expression
Hypotheses	sltsubadd.1	|- ( ph -> A e. No )
	sltsubadd.2	|- ( ph -> B e. No )
	sltsubadd.3	|- ( ph -> C e. No )
Assertion	sltaddsub2d	|- ( ph -> ( ( A +s B ) B

Proof

Step	Hyp	Ref	Expression
1		sltsubadd.1	|- ( ph -> A e. No )
2		sltsubadd.2	|- ( ph -> B e. No )
3		sltsubadd.3	|- ( ph -> C e. No )
4	1 2	addscomd	|- ( ph -> ( A +s B ) = ( B +s A ) )
5	4	breq1d	|- ( ph -> ( ( A +s B ) ( B +s A )
6	2 1 3	sltaddsubd	|- ( ph -> ( ( B +s A ) B
7	5 6	bitrd	|- ( ph -> ( ( A +s B ) B