Theorem pncan3oi

Description: Subtraction and addition of equals. Almost but not exactly the same as pncan3i and pncan , this order happens often when applying "operations to both sides" so create a theorem specifically for it. A deduction version of this is available as pncand . (Contributed by David A. Wheeler, 11-Oct-2018)

	Ref	Expression
Hypotheses	pncan3oi.1	$$⊢A\in ℂ$$
	pncan3oi.2	$$⊢B\in ℂ$$
Assertion	pncan3oi	$$⊢A+B-B=A$$

Proof

Step	Hyp	Ref	Expression
1		pncan3oi.1	$$⊢A\in ℂ$$
2		pncan3oi.2	$$⊢B\in ℂ$$
3		pncan	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B-B=A$$
4	1 2 3	mp2an	$$⊢A+B-B=A$$