This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = ( A - C ) <-> B = C ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
2 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
3 1 2 addcomd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B + A ) = ( A + B ) )
4 3 eqeq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + A ) = ( A + C ) <-> ( A + B ) = ( A + C ) ) )
5 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
6 addsubeq4 
 |-  ( ( ( B e. CC /\ A e. CC ) /\ ( A e. CC /\ C e. CC ) ) -> ( ( B + A ) = ( A + C ) <-> ( A - B ) = ( A - C ) ) )
7 1 2 2 5 6 syl22anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + A ) = ( A + C ) <-> ( A - B ) = ( A - C ) ) )
8 addcan 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) = ( A + C ) <-> B = C ) )
9 4 7 8 3bitr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = ( A - C ) <-> B = C ) )