This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A = B

Proof

Step Hyp Ref Expression
1 subcl ⊢ B ∈ ℂ ∧ A ∈ ℂ → B − A ∈ ℂ
2 eqid ⊢ B − A = B − A
3 subadd ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ B − A ∈ ℂ → B − A = B − A ↔ A + B - A = B
4 2 3 mpbii ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ B − A ∈ ℂ → A + B - A = B
5 1 4 mpd3an3 ⊢ B ∈ ℂ ∧ A ∈ ℂ → A + B - A = B
6 5 ancoms ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - A = B