Theorem slesubd

Description: Swap subtrahends in a surreal inequality. (Contributed by Scott Fenton, 29-Jan-2026)

	Ref	Expression
Hypotheses	slesubd.1	|- ( ph -> A e. No )
	slesubd.2	|- ( ph -> B e. No )
	slesubd.3	|- ( ph -> C e. No )
Assertion	slesubd	|- ( ph -> ( A <_s ( B -s C ) <-> C <_s ( B -s A ) ) )

Proof

Step	Hyp	Ref	Expression
1		slesubd.1	|- ( ph -> A e. No )
2		slesubd.2	|- ( ph -> B e. No )
3		slesubd.3	|- ( ph -> C e. No )
4		npcans	|- ( ( B e. No /\ A e. No ) -> ( ( B -s A ) +s A ) = B )
5	2 1 4	syl2anc	|- ( ph -> ( ( B -s A ) +s A ) = B )
6	2 1	subscld	|- ( ph -> ( B -s A ) e. No )
7	1 6	addscomd	|- ( ph -> ( A +s ( B -s A ) ) = ( ( B -s A ) +s A ) )
8		npcans	|- ( ( B e. No /\ C e. No ) -> ( ( B -s C ) +s C ) = B )
9	2 3 8	syl2anc	|- ( ph -> ( ( B -s C ) +s C ) = B )
10	5 7 9	3eqtr4rd	|- ( ph -> ( ( B -s C ) +s C ) = ( A +s ( B -s A ) ) )
11	10	breq2d	|- ( ph -> ( ( A +s C ) <_s ( ( B -s C ) +s C ) <-> ( A +s C ) <_s ( A +s ( B -s A ) ) ) )
12	2 3	subscld	|- ( ph -> ( B -s C ) e. No )
13	1 12 3	sleadd1d	|- ( ph -> ( A <_s ( B -s C ) <-> ( A +s C ) <_s ( ( B -s C ) +s C ) ) )
14	3 6 1	sleadd2d	|- ( ph -> ( C <_s ( B -s A ) <-> ( A +s C ) <_s ( A +s ( B -s A ) ) ) )
15	11 13 14	3bitr4d	|- ( ph -> ( A <_s ( B -s C ) <-> C <_s ( B -s A ) ) )