Metamath Proof Explorer

Theorem subcani

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

Ref Expression
Hypotheses negidi.1 ⊢ A ∈ ℂ
pncan3i.2 ⊢ B ∈ ℂ
subadd.3 ⊢ C ∈ ℂ
Assertion subcani ⊢ A − B = A − C ↔ B = C

Proof

Step Hyp Ref Expression
1 negidi.1 ⊢ A ∈ ℂ
2 pncan3i.2 ⊢ B ∈ ℂ
3 subadd.3 ⊢ C ∈ ℂ
4 subcan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A − B = A − C ↔ B = C
5 1 2 3 4 mp3an ⊢ A − B = A − C ↔ B = C