Metamath Proof Explorer

Theorem subcan2

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ∈ ℂ
2 simp3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ∈ ℂ
3 subcl ⊢ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ
4 3 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B − C ∈ ℂ
5 subadd2 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ B − C ∈ ℂ → A − C = B − C ↔ B - C + C = A
6 1 2 4 5 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C = B − C ↔ B - C + C = A
7 npcan ⊢ B ∈ ℂ ∧ C ∈ ℂ → B - C + C = B
8 7 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B - C + C = B
9 8 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B - C + C = A ↔ B = A
10 eqcom ⊢ B = A ↔ A = B
11 9 10 bitrdi ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B - C + C = A ↔ A = B
12 6 11 bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − C = B − C ↔ A = B