Theorem nncansd

Description: Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Hypotheses	nncansd.1	|- ( ph -> A e. No )
	nncansd.2	|- ( ph -> B e. No )
Assertion	nncansd	|- ( ph -> ( A -s ( A -s B ) ) = B )

Proof

Step	Hyp	Ref	Expression
1		nncansd.1	|- ( ph -> A e. No )
2		nncansd.2	|- ( ph -> B e. No )
3	1 1 2	subsubs2d	|- ( ph -> ( A -s ( A -s B ) ) = ( A +s ( B -s A ) ) )
4		pncan3s	|- ( ( A e. No /\ B e. No ) -> ( A +s ( B -s A ) ) = B )
5	1 2 4	syl2anc	|- ( ph -> ( A +s ( B -s A ) ) = B )
6	3 5	eqtrd	|- ( ph -> ( A -s ( A -s B ) ) = B )