Theorem repncan3

Description: Addition and subtraction of equals. Based on pncan3 . (Contributed by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Assertion	repncan3	|- ( ( A e. RR /\ B e. RR ) -> ( A + ( B -R A ) ) = B )

Proof

Step	Hyp	Ref	Expression
1		rersubcl	|- ( ( B e. RR /\ A e. RR ) -> ( B -R A ) e. RR )
2		eqid	|- ( B -R A ) = ( B -R A )
3		resubadd	|- ( ( B e. RR /\ A e. RR /\ ( B -R A ) e. RR ) -> ( ( B -R A ) = ( B -R A ) <-> ( A + ( B -R A ) ) = B ) )
4	2 3	mpbii	|- ( ( B e. RR /\ A e. RR /\ ( B -R A ) e. RR ) -> ( A + ( B -R A ) ) = B )
5	1 4	mpd3an3	|- ( ( B e. RR /\ A e. RR ) -> ( A + ( B -R A ) ) = B )
6	5	ancoms	|- ( ( A e. RR /\ B e. RR ) -> ( A + ( B -R A ) ) = B )