Theorem mteqand

Description: A modus tollens deduction for inequality. (Contributed by Steven Nguyen, 1-Jun-2023)

	Ref	Expression
Hypotheses	mteqand.1	|- ( ph -> C =/= D )
	mteqand.2	|- ( ( ph /\ A = B ) -> C = D )
Assertion	mteqand	|- ( ph -> A =/= B )

Proof

Step	Hyp	Ref	Expression
1		mteqand.1	|- ( ph -> C =/= D )
2		mteqand.2	|- ( ( ph /\ A = B ) -> C = D )
3	1	neneqd	|- ( ph -> -. C = D )
4	3 2	mtand	|- ( ph -> -. A = B )
5	4	neqned	|- ( ph -> A =/= B )