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

Metamath Proof Explorer

Theorem npncan3

Description: Cancellation law for subtraction. (Contributed by Scott Fenton, 23-Jun-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion npncan3 
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( C - A ) ) = ( C - B ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
2 subcl 
 |-  ( ( C e. CC /\ A e. CC ) -> ( C - A ) e. CC )
3 2 ancoms 
 |-  ( ( A e. CC /\ C e. CC ) -> ( C - A ) e. CC )
4 3 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C - A ) e. CC )
5 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
6 addsub 
 |-  ( ( A e. CC /\ ( C - A ) e. CC /\ B e. CC ) -> ( ( A + ( C - A ) ) - B ) = ( ( A - B ) + ( C - A ) ) )
7 1 4 5 6 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + ( C - A ) ) - B ) = ( ( A - B ) + ( C - A ) ) )
8 pncan3 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A + ( C - A ) ) = C )
9 8 3adant2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( C - A ) ) = C )
10 9 oveq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + ( C - A ) ) - B ) = ( C - B ) )
11 7 10 eqtr3d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) + ( C - A ) ) = ( C - B ) )