Theorem mteqand 3051

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

Hypotheses

Ref	Expression
mteqand.1	⊢ (𝜑 → 𝐶 ≠ 𝐷)
mteqand.2	⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷)

Assertion

Ref	Expression
mteqand	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem mteqand

Step	Hyp	Ref	Expression
1		mteqand.1	. . . 4 ⊢ (𝜑 → 𝐶 ≠ 𝐷)
2	1	neneqd 2965	. . 3 ⊢ (𝜑 → ¬ 𝐶 = 𝐷)
3		mteqand.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷)
4	2, 3	mtand 827	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
5	4	neqned 2967	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401  df-ne 2961

This theorem is referenced by:  isdrngd  20838  imadrhmcl  20869  qsidomlem2  21441  tglnpt3  28881  fracfld  33544  rprmasso  33732  vr1nz  33800  rtelextdg2lem  34033  2sqr3minply  34087  cos9thpiminplylem2  34090  zarcmplem  34188  expeq1d  42945  remul01  43028  remulinvcom  43054  mulgt0b2d  43112  sn-inelr  43121  ricdrng1  43158  prjspersym  43201  prjspreln0  43203  prjspner1  43220  flt0  43231  fltne  43238  eufunc  50151