Theorem mteqand 3055

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 2969	. . 3 ⊢ (𝜑 → ¬ 𝐶 = 𝐷)
3		mteqand.2	. . 3 ⊢ ((𝜑 ∧ 𝐴 = 𝐵) → 𝐶 = 𝐷)
4	2, 3	mtand 827	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
5	4	neqned 2971	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ≠ wne 2964

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 2965

This theorem is referenced by:  isdrngd  20847  imadrhmcl  20878  qsidomlem2  21450  tglnpt3  28889  fracfld  33572  rprmasso  33760  vr1nz  33828  rtelextdg2lem  34061  2sqr3minply  34115  cos9thpiminplylem2  34118  zarcmplem  34216  expeq1d  42975  remul01  43058  remulinvcom  43084  mulgt0b2d  43142  sn-inelr  43151  ricdrng1  43188  prjspersym  43231  prjspreln0  43233  prjspner1  43250  flt0  43261  fltne  43268  eufunc  50185