Theorem mteqand 3047

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ne 2957

This theorem is used by:  isdrngd  21002  imadrhmcl  21034  qsidomlem2  21617  flt0  27951  fltne  27957  tglnpt3  29104  tgaaddcpbl  29334  angmgmaddeu3  29363  prlngmid2  29421  prlngsymquadlem  29423  fracfld  33852  rprmasso  34039  vr1nz  34107  rtelextdg2lem  34340  2sqr3minply  34394  cos9thpiminplylem2  34397  zarcmplem  34495  expeq1d  43349  remul01  43426  remulinvcom  43452  mulgt0b2d  43510  sn-inelr  43519  ricdrng1  43554  prjspersym  43597  prjspreln0  43599  prjspner1  43616  eufunc  50574