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