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	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-A=B$$

Proof

Step	Hyp	Ref	Expression
1		subcl	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to B-A\in ℂ$$
2		eqid	$$⊢B-A=B-A$$
3		subadd	$$⊢\left(B\in ℂ\wedge A\in ℂ\wedge B-A\in ℂ\right)\to \left(B-A=B-A\leftrightarrow A+B-A=B\right)$$
4	2 3	mpbii	$$⊢\left(B\in ℂ\wedge A\in ℂ\wedge B-A\in ℂ\right)\to A+B-A=B$$
5	1 4	mpd3an3	$$⊢\left(B\in ℂ\wedge A\in ℂ\right)\to A+B-A=B$$
6	5	ancoms	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-A=B$$