Theorem addcani

Description: Cancellation law for addition. Theorem I.1 of Apostol p. 18. (Contributed by NM, 27-Oct-1999) (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	addcani	|- ( ( A + B ) = ( A + C ) <-> B = C )

Proof

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