Metamath Proof Explorer

Theorem addsubeq4com

Description: Relation between sums and differences. (Contributed by Steven Nguyen, 5-Jan-2023)

Ref Expression
Assertion addsubeq4com ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B = C + D ↔ A − C = D − B

Proof

Step Hyp Ref Expression
1 eqcom ⊢ A + B = C + D ↔ C + D = A + B
2 addsubeq4 ⊢ C ∈ ℂ ∧ D ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → C + D = A + B ↔ A − C = D − B
3 2 ancoms ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → C + D = A + B ↔ A − C = D − B
4 1 3 bitrid ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ → A + B = C + D ↔ A − C = D − B