Theorem mteqand 3046

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

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

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 2956

This theorem is used by:  isdrngd  21028  imadrhmcl  21060  qsidomlem2  21643  flt0  27975  fltne  27981  tglnpt3  29128  tgaaddcpbl  29358  angmgmaddeu3  29387  prlngmid2  29445  prlngsymquadlem  29447  fracfld  33917  rprmasso  34104  vr1nz  34172  rtelextdg2lem  34405  2sqr3minply  34459  cos9thpiminplylem2  34462  zarcmplem  34560  expeq1d  43475  remul01  43552  remulinvcom  43578  mulgt0b2d  43636  sn-inelr  43645  ricdrng1  43686  prjspersym  43729  prjspreln0  43731  line2x  49960  fucoaltnelem  50588  eufunc  50751