Theorem pncan3s

Description: Subtraction and addition of equals. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	pncan3s	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐵 -s 𝐴 ) = ( 𝐵 -s 𝐴 )
2		simpr	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐵 ∈ No )
3		simpl	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → 𝐴 ∈ No )
4	2 3	subscld	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐵 -s 𝐴 ) ∈ No )
5	2 3 4	subaddsd	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( 𝐵 -s 𝐴 ) = ( 𝐵 -s 𝐴 ) ↔ ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) = 𝐵 ) )
6	1 5	mpbii	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s ( 𝐵 -s 𝐴 ) ) = 𝐵 )