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