# Metamath Proof Explorer

## Theorem subcan2

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

Ref Expression
Assertion subcan2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{C}={B}-{C}↔{A}={B}\right)$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {A}\in ℂ$
2 simp3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {C}\in ℂ$
3 subcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}\in ℂ$
4 3 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}\in ℂ$
5 subadd2 ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {B}-{C}\in ℂ\right)\to \left({A}-{C}={B}-{C}↔{B}-{C}+{C}={A}\right)$
6 1 2 4 5 syl3anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{C}={B}-{C}↔{B}-{C}+{C}={A}\right)$
7 npcan ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}+{C}={B}$
8 7 3adant1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to {B}-{C}+{C}={B}$
9 8 eqeq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({B}-{C}+{C}={A}↔{B}={A}\right)$
10 eqcom ${⊢}{B}={A}↔{A}={B}$
11 9 10 syl6bb ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({B}-{C}+{C}={A}↔{A}={B}\right)$
12 6 11 bitrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {C}\in ℂ\right)\to \left({A}-{C}={B}-{C}↔{A}={B}\right)$