Metamath Proof Explorer

Theorem subadd2

Description: Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 subadd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B = C ↔ B + C = A
2 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ∈ ℂ
3 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
4 2 3 addcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
5 4 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C = A ↔ C + B = A
6 1 5 bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B = C ↔ C + B = A