Theorem repncan3

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

	Ref	Expression
Assertion	repncan3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( 𝐵 −ℝ 𝐴 ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		rersubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐵 −ℝ 𝐴 ) ∈ ℝ )
2		eqid	⊢ ( 𝐵 −ℝ 𝐴 ) = ( 𝐵 −ℝ 𝐴 )
3		resubadd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐵 −ℝ 𝐴 ) ∈ ℝ ) → ( ( 𝐵 −ℝ 𝐴 ) = ( 𝐵 −ℝ 𝐴 ) ↔ ( 𝐴 + ( 𝐵 −ℝ 𝐴 ) ) = 𝐵 ) )
4	2 3	mpbii	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐵 −ℝ 𝐴 ) ∈ ℝ ) → ( 𝐴 + ( 𝐵 −ℝ 𝐴 ) ) = 𝐵 )
5	1 4	mpd3an3	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 + ( 𝐵 −ℝ 𝐴 ) ) = 𝐵 )
6	5	ancoms	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( 𝐵 −ℝ 𝐴 ) ) = 𝐵 )