Metamath Proof Explorer

Theorem subcan

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ
2 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ
3 1 2 addcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+A=A+B
4 3 eqeq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+A=A+C↔A+B=A+C
5 simp3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ
6 addsubeq4 ⊢B∈ℂ∧A∈ℂ∧A∈ℂ∧C∈ℂ→B+A=A+C↔A−B=A−C
7 1 2 2 5 6 syl22anc ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+A=A+C↔A−B=A−C
8 addcan ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A+B=A+C↔B=C
9 4 7 8 3bitr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=A−C↔B=C