Theorem mteqand 3052

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

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

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 2962

This theorem is used by:  isdrngd  20905  imadrhmcl  20937  qsidomlem2  21518  tglnpt3  28964  prlngmid2  29248  prlngsymquadlem  29250  fracfld  33660  rprmasso  33846  vr1nz  33914  rtelextdg2lem  34147  2sqr3minply  34201  cos9thpiminplylem2  34204  zarcmplem  34302  expeq1d  43126  remul01  43209  remulinvcom  43235  mulgt0b2d  43293  sn-inelr  43302  ricdrng1  43337  prjspersym  43380  prjspreln0  43382  prjspner1  43399  flt0  43410  fltne  43417  eufunc  50341