Theorem mteqand 3031

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ≠ wne 2938

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 207  df-an 396  df-ne 2939

This theorem is referenced by:  isdrngd  20782  imadrhmcl  20815  fracfld  33290  qsidomlem2  33461  rprmasso  33533  rtelextdg2lem  33732  2sqr3minply  33753  zarcmplem  33842  expeq1d  42338  remul01  42414  remulinvcom  42439  ricdrng1  42515  prjspersym  42594  prjspreln0  42596  prjspner1  42613  flt0  42624  fltne  42631