Metamath Proof Explorer

Theorem subsub23

Description: Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 addcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
2 1 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C = C + B
3 2 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B + C = A ↔ C + B = A
4 subadd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B = C ↔ B + C = A
5 subadd ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B ∈ ℂ → A − C = B ↔ C + B = A
6 5 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C = B ↔ C + B = A
7 3 4 6 3bitr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B = C ↔ A − C = B