Theorem addcan2i

Description: Cancellation law for addition. Theorem I.1 of Apostol p. 18. (Contributed by NM, 14-May-2003) (Revised by Scott Fenton, 3-Jan-2013)

	Ref	Expression
Hypotheses	mul.1	|- A e. CC
	mul.2	|- B e. CC
	mul.3	|- C e. CC
Assertion	addcan2i	|- ( ( A + C ) = ( B + C ) <-> A = B )

Proof

Step	Hyp	Ref	Expression
1		mul.1	|- A e. CC
2		mul.2	|- B e. CC
3		mul.3	|- C e. CC
4		addcan2	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + C ) = ( B + C ) <-> A = B ) )
5	1 2 3 4	mp3an	|- ( ( A + C ) = ( B + C ) <-> A = B )