Theorem pncan3s

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

	Ref	Expression
Assertion	pncan3s	|- ( ( A e. No /\ B e. No ) -> ( A +s ( B -s A ) ) = B )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( B -s A ) = ( B -s A )
2		simpr	|- ( ( A e. No /\ B e. No ) -> B e. No )
3		simpl	|- ( ( A e. No /\ B e. No ) -> A e. No )
4	2 3	subscld	|- ( ( A e. No /\ B e. No ) -> ( B -s A ) e. No )
5	2 3 4	subaddsd	|- ( ( A e. No /\ B e. No ) -> ( ( B -s A ) = ( B -s A ) <-> ( A +s ( B -s A ) ) = B ) )
6	1 5	mpbii	|- ( ( A e. No /\ B e. No ) -> ( A +s ( B -s A ) ) = B )