Theorem mteqand 3024

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ≠ wne 2933

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 2934

This theorem is referenced by:  isdrngd  20730  imadrhmcl  20762  fracfld  33307  qsidomlem2  33473  rprmasso  33545  vr1nz  33608  rtelextdg2lem  33765  2sqr3minply  33819  cos9thpiminplylem2  33822  zarcmplem  33917  expeq1d  42340  remul01  42417  remulinvcom  42442  ricdrng1  42518  prjspersym  42597  prjspreln0  42599  prjspner1  42616  flt0  42627  fltne  42634  eufunc  49374