Theorem addneintrd

Description: Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad . Consequence of addcand . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	muld.1	$$⊢\phi \to A\in ℂ$$
	addcomd.2	$$⊢\phi \to B\in ℂ$$
	addcand.3	$$⊢\phi \to C\in ℂ$$
	addneintrd.4	$$⊢\phi \to B\ne C$$
Assertion	addneintrd	$$⊢\phi \to A+B\ne A+C$$

Proof

Step	Hyp	Ref	Expression
1		muld.1	$$⊢\phi \to A\in ℂ$$
2		addcomd.2	$$⊢\phi \to B\in ℂ$$
3		addcand.3	$$⊢\phi \to C\in ℂ$$
4		addneintrd.4	$$⊢\phi \to B\ne C$$
5	1 2 3	addcand	$$⊢\phi \to \left(A+B=A+C\leftrightarrow B=C\right)$$
6	5	necon3bid	$$⊢\phi \to \left(A+B\ne A+C\leftrightarrow B\ne C\right)$$
7	4 6	mpbird	$$⊢\phi \to A+B\ne A+C$$