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