Theorem mteqand 3048

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

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

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 2958

This theorem is used by:  isdrngd  20937  imadrhmcl  20969  qsidomlem2  21550  tglnpt3  29009  tgaaddcpbl  29239  angmgmaddeu3  29268  prlngmid2  29326  prlngsymquadlem  29328  fracfld  33757  rprmasso  33943  vr1nz  34011  rtelextdg2lem  34244  2sqr3minply  34298  cos9thpiminplylem2  34301  zarcmplem  34399  expeq1d  43207  remul01  43290  remulinvcom  43316  mulgt0b2d  43374  sn-inelr  43383  ricdrng1  43418  prjspersym  43461  prjspreln0  43463  prjspner1  43480  flt0  43491  fltne  43498  eufunc  50456