Theorem mteqand 3049

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ≠ wne 2958

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 2959

This theorem is referenced by:  isdrngd  20850  imadrhmcl  20881  qsidomlem2  21462  tglnpt3  28905  prlngmid2  29189  prlngsymquadlem  29191  fracfld  33607  rprmasso  33793  vr1nz  33861  rtelextdg2lem  34094  2sqr3minply  34148  cos9thpiminplylem2  34151  zarcmplem  34249  expeq1d  43063  remul01  43146  remulinvcom  43172  mulgt0b2d  43230  sn-inelr  43239  ricdrng1  43276  prjspersym  43319  prjspreln0  43321  prjspner1  43338  flt0  43349  fltne  43356  eufunc  50277