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

Metamath Proof Explorer

Theorem cnapbmcpd

Description: ((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
2 1 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B ∈ ℂ
3 simpr ⊢ C ∈ ℂ ∧ D ∈ ℂ → D ∈ ℂ
4 3 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → D ∈ ℂ
5 simpl ⊢ C ∈ ℂ ∧ D ∈ ℂ → C ∈ ℂ
6 5 adantl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → C ∈ ℂ
7 2 4 6 addsubd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + D - C = A + B - C + D
8 simpl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ∈ ℂ
9 8 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A ∈ ℂ
10 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ → B ∈ ℂ
11 10 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → B ∈ ℂ
12 9 11 4 add32d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + D = A + D + B
13 12 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B + D - C = A + D + B - C
14 7 13 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B - C + D = A + D + B - C