Theorem nncansd

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

	Ref	Expression
Hypotheses	nncansd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	nncansd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
Assertion	nncansd	⊢ ( 𝜑 → ( 𝐴 -s ( 𝐴 -s 𝐵 ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nncansd.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		nncansd.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3	1 1 2	subsubs2d	⊢ ( 𝜑 → ( 𝐴 -s ( 𝐴 -s 𝐵 ) ) = ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) )
4		pncan3s	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) = 𝐵 )
5	1 2 4	syl2anc	⊢ ( 𝜑 → ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) = 𝐵 )
6	3 5	eqtrd	⊢ ( 𝜑 → ( 𝐴 -s ( 𝐴 -s 𝐵 ) ) = 𝐵 )