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

Metamath Proof Explorer

Theorem subadd23

Description: Commutative/associative law for addition and subtraction. (Contributed by NM, 1-Feb-2007)

Ref Expression
Assertion subadd23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B + C = A + C - B

Proof

Step Hyp Ref Expression
1 addsub ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + C - B = A - B + C
2 addsubass ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A + C - B = A + C - B
3 1 2 eqtr3d ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A - B + C = A + C - B
4 3 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A - B + C = A + C - B