Theorem pncan3

Description: Subtraction and addition of equals. (Contributed by NM, 14-Mar-2005) (Proof shortened by Steven Nguyen, 8-Jan-2023)

	Ref	Expression
Assertion	pncan3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + ( 𝐵 − 𝐴 ) ) = 𝐵 )

Proof

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